Giáo trình Đặc tả hình thức - Chương 14: JML nâng cao - Nguyễn Thị Minh Tuyền

Nội dung text: Giáo trình Đặc tả hình thức - Chương 14: JML nâng cao - Nguyễn Thị Minh Tuyền

1. LOGO Đặc tả hình thức JML nâng cao Nguyễn Thị Minh Tuyền Nội dung slide này được dịch từ các slide của David Cok, Joe Kiniry, Eric Poll 1
2. 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 Nguyễn Thị Minh Tuyền 2 Đặc tả hình thức
3. 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 Nguyễn Thị Minh Tuyền 3 Đặc tả hình thức
4. v Visibility Nguyễn Thị Minh Tuyền 4 Đặc tả hình thức
5. 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. Nguyễn Thị Minh Tuyền 5 Đặc tả hình thức
6. 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; // WRONG !! public void pub2(int i) { } Nguyễn Thị Minh Tuyền 6 Đặc tả hình thức
7. 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. Nguyễn Thị Minh Tuyền 7 Đặc tả hình thức
8. v Ngoại lệ và JML Nguyễn Thị Minh Tuyền 8 Đặc tả hình thức
9. Đặ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. Nguyễn Thị Minh Tuyền 9 Đặc tả hình thức
10. 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; Nguyễn Thị Minh Tuyền 10 Đặc tả hình thức
11. 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ệ. Nguyễn Thị Minh Tuyền 11 Đặc tả hình thức
12. Đặ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; Nguyễn Thị Minh Tuyền 12 Đặc tả hình thức
13. Đặ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; Nguyễn Thị Minh Tuyền 13 Đặc tả hình thức
14. Đư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 Nguyễn Thị Minh Tuyền 14 Đặc tả hình thức
15. 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 Nguyễn Thị Minh Tuyền 15 Đặc tả hình thức
16. Ví dụ /*@ normal_behavior requires amount balance signals (BankException e) @*/ public int debit(int amount) throws BankException { } Nguyễn Thị Minh Tuyền 16 Đặc tả hình thức
17. Ví dụ v hay tương đương /*@ requires true; ensures \old(amount balance) && @*/ public int debit(int amount) throws BankException { } Nguyễn Thị Minh Tuyền 17 Đặc tả hình thức
18. 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. Nguyễn Thị Minh Tuyền 18 Đặc tả hình thức
19. v Mệnh đề assignable và nhóm dữ liệu Nguyễn Thị Minh Tuyền 19 Đặc tả hình thức
20. 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[*], ; Nguyễn Thị Minh Tuyền 20 Đặc tả hình thức
21. 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) { } } Nguyễn Thị Minh Tuyền 21 Đặc tả hình thức
22. 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ả. Nguyễn Thị Minh Tuyền 22 Đặc tả hình thức
23. 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. Nguyễn Thị Minh Tuyền 23 Đặc tả hình thức
24. 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) { } } Nguyễn Thị Minh Tuyền 24 Đặc tả hình thức
25. 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() { } } Nguyễn Thị Minh Tuyền 25 Đặc tả hình thức
26. 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() { } } Nguyễn Thị Minh Tuyền 26 Đặc tả hình thức
27. 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. Nguyễn Thị Minh Tuyền 27 Đặc tả hình thức
28. 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. Nguyễn Thị Minh Tuyền 28 Đặc tả hình thức