Đặc tả hình thức - JML nâng cao - Nguyễn Thị Minh Tuyền

LOGO Đặc tả hình thức Nguyễn Thị Minh Tuyền 1 JML nâng cao Nội dung slide này được dịch từ các slide của David Cok, Joe Kiniry, Eric Poll Đặc tả hình thức Từ khóa chính trong JML v requires v ensures v signals v assignable v normal_behavior v invariant v non_null v pure v \old, \forall, \exists, \result 2 Nguyễn Thị Minh Tuyền Đặc tả hình thức Các tính năng nâng cao v Visibility v Đặc tả các ngoại lệ v Mệnh đề assignable và nhóm dữ liệu v Aliasing v Thừa kế đặc tả, ensuring behavioural subtyping v Các trường chỉ ở mức đặc tả: ghost và model v Ngữ nghĩa của invariant 3 Nguyễn Thị Minh Tuyền Đặc tả hình thức v Visibility 4 Nguyễn Thị Minh Tuyền Đặc tả hình thức Visibility v JML áp dụng các quy tắt về visibility tương tự như Java. v Ví dụ: public class Bag{ ... private int n; //@ requires n > 0; public int extractMin(){ ... } không phải là kiểu hợp lệ, vì visibility của phương thức extractMin là public chỉ đến trường n có visibility là private. 5 Nguyễn Thị Minh Tuyền Đặc tả hình thức Visibility public int pub; private int priv; //@ requires i <= pub; public void pub1 (int i) { ... } //@ requires i <= pub && i <= priv; private void priv1 (int i) ... //@ requires i <= pub && i <= priv; public void pub2(int i) { ... } 6 Nguyễn Thị Minh Tuyền // WRONG !! Đặc tả hình thức Visibility: spec_public v  Từ khóa spec_public nới lỏng visibility cho các đặc tả. Trường private với spec_public sẽ được cho phép ở mức đặc tả với visibility là public. v  Ví dụ: public class Bag{ ... private /*@ spec_public @*/ int n; //@ requires n > 0; public int extractMin(){ ... } v  Buộc các thông tin private thành public tất nhiên là không đẹp mắt xíu nào. v  Có một cách biểu diễn đẹp mắt hơn đó là khai báo các trường với từ khóa model để biểu diễn các chi tiết được cài đặt private. 7 Nguyễn Thị Minh Tuyền Đặc tả hình thức v Ngoại lệ và JML 8 Nguyễn Thị Minh Tuyền Đặc tả hình thức Đặc tả các ngoại lệ v Đặc tả phương thức có thể (không) cho phép đưa ra các ngoại lệ, và đặc tả điều kiện sau của ngoại lệ phải đúng khi một ngoại lệ được đưa ra. v Có một số nguyên tắc (không) cho phép các ngoại lệ. v Cảnh báo: các đặc tả ngoại lệ rất dễ sai. v Không cho phép bất cứ ngoại lệ nào được đưa ra là phương pháp đơn giản nhất. 9 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ngoại lệ được cho phép bởi đặc tả v Mặc định, một phương thức được phép đưa ra ngoại lệ, nhưng chỉ những ngoại lệ nào nằm trong danh sách của mệnh đề throws. Vì vậy //@ requires 0 <= amount && amount <= balance; public int debit(int amount) throws BankException { ... } v có một mệnh đề //@ signals (BankException) true; v và một mệnh đề //@ signals (Exception e) e instanceof BankException; 10 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ngoại lệ được cho phép bởi đặc tả v Mặc định, phương thức cho phép đưa ra các ngoại lệ, nhưng chỉ ngoại lệ nào nằm trong mệnh đề throws. Vì vậy: public int debit(int amount) { ... } v có một mệnh đề //@ signals (Exception) false; debit không được phép đưa ra các ngoại lệ. 11 Nguyễn Thị Minh Tuyền Đặc tả hình thức Đặt ra luật cho ngoại lệ v Để cấm một số ngoại lệ SomeException nào đó: §  loại bỏ nó ra khỏi mệnh đề throws (chỉ có thể cho các ngoại lệ không được kiểm tra). §  thêm một mệnh đề signals: //@ signals (SomeException) false; §  hạn chế tập các ngoại lệ được cho phép, sử dụng một điều kiện sau như: /*@ signals (Exception e) e instanceof E1 || ... || e instanceof En;*/ §  hoặc tương được, ta có thể dùng: //@ signals_only E1, ... En; 12 Nguyễn Thị Minh Tuyền Đặc tả hình thức Đặt ra luật cho ngoại lệ v Để cấm tất cả các ngoại lệ: §  Bỏ qua tất cả các ngoại lệ từ mệnh đề throws (chỉ có thể cho các ngoại lệ không được kiểm tra). §  Thêm vào một chỉ dẫn signals (Exception) false; §  Sử dụng từ khóa normal_behavior để loại bỏ tất cả các ngoại lệ. /*@ normal_behavior requires ... ensures ... @*/ §  Từ khóa normal_behavior đã ám chỉ signal (Exception) false; 13 Nguyễn Thị Minh Tuyền Đặc tả hình thức Đưa ra một ngoại lệ v Nhận thức được sự khác nhau giữa: §  (1) Nếu P đúng thì SomeException được đưa ra và §  (2) Nếu SomeException được đưa ra thì P đúng v Hai phát biểu trên rất dễ bị nhầm lẫn. §  (2) có thể được phát biểu với signals §  (1) có thể được phát biểu với exceptional_behavior 14 Nguyễn Thị Minh Tuyền Đặc tả hình thức exceptional_behavior /*@ exceptional_behavior requires amount > balance signals (BankException e) e.getReason.equals("Amount too big") @*/ public int debit(int amount) throws BankException { ... } v chỉ ra rằng một BankException phải được đưa ra nếu amout>balance. v normal_behavior ám chỉ rằng signal (Exception) false v exceptional_behavior ám chỉ rằng ensures false 15 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ /*@ normal_behavior requires amount <= balance; ensures ... also exceptional_behavior requires amount > balance signals (BankException e) ... @*/ public int debit(int amount) throws BankException { ... } 16 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ v hay tương đương /*@ requires true; ensures \old(amount<=balance) && ... signals (BankException e) \old(amount>balance) && ... @*/ public int debit(int amount) throws BankException { ... } 17 Nguyễn Thị Minh Tuyền Đặc tả hình thức Hành vi ngoại lệ v Tinh thần: để giữ mọi thứ đơn giản, không cho phép ngoại lệ trong đặc tả bất cứ khi nào có thể. v Ví dụ: Với public void arraycopy(int[] src, int destOffset, int[] dest, int destOffset, int length) throws NullPointerException, ArrayIndexOutOfBoundsException §  viết một đặc tả không cho phép đưa ra bất kỳ ngoại lệ nào và chỉ chú ý đến đặc tả hành vi ngoại lệ nếu thật cần thiết. 18 Nguyễn Thị Minh Tuyền Đặc tả hình thức v Mệnh đề assignable và nhóm dữ liệu 19 Nguyễn Thị Minh Tuyền Đặc tả hình thức Các vấn đề với mệnh đề assignable v Mệnh đề assignable §  Có xu hướng chỉ ra chi tiết cài đặt private /*@ spec_public @*/ int x; ... //@ assignable x, ....; public void m(...) {....} §  Có xu hướng trở nên rất dài //@ assignable x, y, z[*], ....; §  Có xu hướng liệt kê //@ assignable x, f.x, g.y, h.z[*], ....; 20 Nguyễn Thị Minh Tuyền Đặc tả hình thức Các vấn đề với mệnh đề assignable public class Timer{ /*@ spec_public @*/ int time_hrs, time_mins, time_secs; /*@ spec_public @*/ int alarm_hrs, alarm_mins, alarm_secs; //@ assignable time_hrs, time_mins, time_secs; public void tick() { ... } //@ assignable alarm_hrs, alarm_mins, alarm_secs ; public void setAlarm(int hrs, int mins, int secs) { ... } } 21 Nguyễn Thị Minh Tuyền Đặc tả hình thức Giải pháp: nhóm dữ liệu public class Timer{ //@ public model JMLDatagroup time, alarm; int time_hrs, time_mins, time_secs; //@ in time; int alarm_hrs, alarm_mins, alarm_secs; //@ in alarm; //@ assignable time; public void tick() { ... } //@ assignable alarm; public void setAlarm(int hrs, int mins, int secs) { ... } } v time và alarm là các trường model, các trường chỉ có trong đặc tả. 22 Nguyễn Thị Minh Tuyền Đặc tả hình thức Nhóm dữ liệu v Nhóm dữ liệu cung cấp một cơ chế trừu tượng cho mệnh đề assignable v Nhóm dữ liệu mặc định objectState được định nghĩa trong Object.java v Nên khai báo rằng tất cả các trường instance trong objectSate. 23 Nguyễn Thị Minh Tuyền Đặc tả hình thức Nhóm dữ liệu có thể bị lồng nhau public class Timer{ //@ public model JMLDatagroup time, alarm;//@ in objectState; int time_hrs, time_mins, time_secs; //@ in time; int alarm_hrs, alarm_mins, alarm_secs; //@ in alarm; //@ assignable time; public void tick() { ... } //@ assignable alarm; public void setAlarm(int hrs, int mins, int secs) { ... } } 24 Nguyễn Thị Minh Tuyền Đặc tả hình thức assignable và mảng v Một cài đặt khác, sử dụng một mảng gồm 6 chữ số để biểu diễn giờ:phút:giây public class ArrayTimer{ /*@ spec_public @*/ char[] currentTime; //@ invariant currentTime != null; //@ invariant currentTime.length == 6; //@ assignable currentTime[*]; public void tick() { ... } ... } 25 Nguyễn Thị Minh Tuyền Đặc tả hình thức Nhóm dữ liệu và mảng v Một cài đặt khác, sử dụng một mảng gồm 6 chữ số để biểu diễn giờ:phút:giây public class ArrayTimer{ //@ public model JMLDatagroup time; char[] currentTime; //@ in time; //@ maps currentTime[*] \into time; //@ invariant currentTime != null; //@ invariant currentTime.length == 6; //@ assignable time; public void tick() { ... } ... } 26 Nguyễn Thị Minh Tuyền Đặc tả hình thức Nhóm dữ liệu và giao diện v Các nhóm dữ liệu thuận tiện trong việc đặc tả cho các giao diện public interface TimerInterface{ //@ model instance public JMLDatagroup time, alarm; //@ assignable time; public void tick(); //@ assignable alarm; public void setAlarm(int hrs, int mins, int secs); } v Các lớp cài đặt cho giao diện này được tự do chọn trường nào nằm trong nhóm dữ liệu. §  Từ khóa instance là cần thiết, vì các trường trong giao diện mặc định là các trường static trong Java. Các giao diện trong Java không có các trường instance, nhưng JML có các trường instance model. 27 Nguyễn Thị Minh Tuyền Đặc tả hình thức Vấn đề với các mệnh đề assignable v Ngoại trừ khả năng trừu tượng hóa cung cấp bởi nhóm dữ liệu, các mệnh đề assignable còn một vướng mắc trong việc đặc tả chương trình và trong kiểm định chương trình. §  Chú ý rằng proof obligation tương ứng với một mệnh đề assignable là rất phức tạp, gồm một quantification trên tất cả các trường không được đề cập trong mệnh đề assignable. 28 Nguyễn Thị Minh Tuyền