Bài giảng Đặc tả hình thức - Bài 12: Giới thiệu về ESC/Java2 - Thủ thuật và cạm bẫy - Nguyễn Thị Minh Tuyền

Nội dung text: Bài giảng Đặc tả hình thức - Bài 12: Giới thiệu về ESC/Java2 - Thủ thuật và cạm bẫy - Nguyễn Thị Minh Tuyền

1. LOGO Đặc tả hình thức Giới thiệu về ESC/Java2 Thủ thuật và cạm bẫy 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. Nội dung 1. Đặc tả thừa kế 2. Aliasing 3. Object invariants 4. Giả thuyết không nhất quán 5. Exposed references 6. \old 7. Viết đặc tả thế nào Nguyễn Thị Minh Tuyền 2 Đặc tả hình thức
3. Nội dung 1. Đặc tả thừa kế 2. Aliasing 3. Object invariants 4. Giả thuyết không nhất quán 5. Exposed references 6. \old 7. Viết đặc tả thế nào Nguyễn Thị Minh Tuyền 3 Đặc tả hình thức
4. Behavioural subtyping v Giả sử rằng Child mở rộng từ Parent § Behavioural subtyping = các đối tượng từ lớp con Child ứng xử giống các đối tượng từ lớp cha Parent. § Nguyên tắc: mã nguồn sẽ ứng xử như mong đợi nếu ta khai báo một đối tượng Child trong đó một đối tượng Parent đã được cài đặt như mong đợi. Nguyễn Thị Minh Tuyền 4 Đặc tả hình thức
5. Behavioural subtyping v Một số ràng buộc bởi behavioural subtyping: § Bất biến trong lớp con mạnh hơn bất biến trong lớp cha. § Đối với mỗi phương thức: • Điều kiện trước trong lớp con yếu hơn điều kiện trước trong lớp cha • Điều kiện sau trong lớp con mạnh hơn điều kiện sau trong lớp cha. v JML đạt được behavioural subtyping bằng kế thừa đặc tả: bất cứ lớp con nào cũng kế thừa đặc tả từ lớp cha của nó. Nguyễn Thị Minh Tuyền 5 Đặc tả hình thức
6. Kế thừa đặc tả cho bất biến v Bất biến được kế thừa từ các lớp con. v Ví dụ: class Parent { //@ invariant invParent; } class Child extends Parent { //@ invariant invChild; } bất biến cho Child là invChild && invParent. Nguyễn Thị Minh Tuyền 6 Đặc tả hình thức
7. Kế thừa đặc tả cho đặc tả của phương thức class Parent { /*@ requires i >= 0; ensures \result >= i; @*/ int m(int i){ } } class Child extends Parent { /*@ also requires i <= 0; ensures \result <= i; @*/ int m(int i){ } } Từ khóa also chỉ ra rằng các đặc tả được kế thừa. Nguyễn Thị Minh Tuyền 7 Đặc tả hình thức
8. Kế thừa đặc tả cho đặc tả của phương thức v Phương thức m trong Child cũng cần phải thỏa mãn đặc tả trong lớp Parent. Vì thế đặc tả đầy đủ cho Child là /*@ requires i>=0; ensures \result>=i; also requires i <=0 ensures \result<=i; @*/ int m(int i){ } } Kết quả của m(0) là gì? Nguyễn Thị Minh Tuyền 8 Đặc tả hình thức
9. Kế thừa đặc tả cho đặc tả của phương thức v Đặc tả này của Child tương đương với class Child extends Parent { /*@ requires i =0; ensures \old(i >= 0) ==> \result >= i; ensures \old(i \result <= i; @*/ int m(int i){ } } Nguyễn Thị Minh Tuyền 9 Đặc tả hình thức
10. Đặc tả thừa kế v Hai Object là == thì cũng luôn luôn equals. Nhưng ngược lại thì không nhất thiết phải đúng. Nó đúng cho các đối tượng mà kiểu động là Object. public class Object { //@ ensures (this == o) ==> \result; /*@ ensures \typeof(this) == \type(Object) ==> (\result == (this==o)); */ public boolean equals(Object o); } Không nhất thiết đúng cho tất cả Đúng cho tất cả các Object các subtype Nguyễn Thị Minh Tuyền 10 Đặc tả hình thức
11. Đặc tả thừa kế v Đặc tả lớp cơ sở áp dụng cho các lớp con § ESC/Java2 tuân theo behavioral subtyping § Đặc tả từ các giao diện được cài đặt cũng phải thỏa mãn các lớp cài đặt. v Giữ lại \typeof(this) == \type( ) nếu cần. v Các giới hạn trên các ngoại lệ như normal_behavior hoặc signal (E e) false; cũng sẽ được áp dụng cho các lớp được dẫn xuất nữa. Nguyễn Thị Minh Tuyền 11 Đặc tả hình thức
12. Nội dung 1. Đặc tả thừa kế 2. Aliasing 3. Object invariants 4. Giả thuyết không nhất quán 5. Exposed references 6. \old 7. Viết đặc tả thế nào Nguyễn Thị Minh Tuyền 12 Đặc tả hình thức
13. Aliasing v Một vấn đề phổ biến nhưng không dễ thấy gây ra các vi phạm về bất biến là aliasing. public class Alias { /*@ non_null */ int[] a = new int[10]; boolean noneg = true; /*@ invariant noneg ==> (\forall int i; 0 =0); */ //@ requires 0 (\forall int i; 0<=i && i <a.length; Nguyễn Thị Minh Tuyền 13 Đặc tả hình thức
14. Aliasing v Một ngữ cảnh phản ví dụ đầy đủ (sử dụng tùy chọn –counterexample) sinh ra, giữa nhiều thông tin khác: brokenObj%0 != this (brokenObj%0).(a@pre:2.24) == tmp0!a:10.4 this.(a@pre:2.24) == tmp0!a:10.4 v đó là, this và một số đối tượng khác (brokenObj) chia sẻ cùng một đối tượng. this brokenObj int noneg int noneg int[] a int[] a một đối tượng int[] Nguyễn Thị Minh Tuyền 14 Đặc tả hình thức
15. Aliasing v Để sửa điều này, khai báo rằng a chỉ được sở hữu bởi đối tượng cha của nó (owner là một trường ghost của java.lang.Object). public class Alias { /*@ non_null */ int[] a = new int[10]; boolean noneg = true; /*@ invariant noneg ==> (\forall int i; 0 =0); */ //@ invariant a.owner == this; this brokenObj //@ requires 0<=i && i < a.length; int noneg int noneg public void insert(int i, int v) { int[] a int[] a a[i] = v; if (v < 0) noneg = false; } một đối tượng int[] một đối tượng int[] public Alias() { //@ set a.owner = this; int[] } int[] owner owner } Nguyễn Thị Minh Tuyền 15 Đặc tả hình thức
16. Aliasing v Một ví dụ khác. Thất bại ở điều kiện sau. public class Alias2 { /*@ non_null */ Inner n = new Inner(); /*@ non_null */ Inner nn = new Inner(); //@ invariant n.owner == this; //@ invariant nn.owner == this; //@ ensures n.i == \old(n.i + 1); public void add() { n.i++; nn.i++; } Alias2(); } class Inner { public int i; //@ ensures i == 0; Inner(); } Nguyễn Thị Minh Tuyền 16 Đặc tả hình thức
17. v Ngữ cảnh phản ví dụ chỉ ra rằng this.(nn:3.24) == tmp0!n:10.4 tmp2!nn:11.4 == tmp0!n:10.4 v n và nn được tham chiếu từ cùng một đối tượng. v Nếu ta thêm bất biến //@ invariant n != nn; để ngăn aliasing giữa hai trường này thì mọi thứ đều ok. Nguyễn Thị Minh Tuyền 17 Đặc tả hình thức
18. Aliasing v Aliasing là một khó khăn lớn trong kiểm định. v Quản lý aliasing là một lĩnh vực nghiên cứu năng động, liên quan đến quản lý các frame condition. v Các trường owner này tạo ra một hình thức đóng gói có thể được kiểm tra bởi ESC/Java để điều khiển cái gì có thể thay đổi bởi một thao tác cho sẵn. Nguyễn Thị Minh Tuyền 18 Đặc tả hình thức
19. Nội dung 1. Đặc tả thừa kế 2. Aliasing 3. Object invariants 4. Giả thuyết không nhất quán 5. Exposed references 6. \old 7. Viết đặc tả thế nào Nguyễn Thị Minh Tuyền 19 Đặc tả hình thức
20. Viết các object invariant v Đảm bảo rằng các bất biến của lớp là về đối tượng. v Các phát biểu về tất cả các đối tượng của một lớp có thể đúng nhưng khó chứng minh, đặc biệt là đối với các công cụ chứng minh tự động. v Ví dụ, nếu có một vị từ P được giả sử là đúng cho các đối tượng có kiểu T, thì không viết: //@ invariant (\forall T t; P(t)); v Thay vào đó, viết: //@ invariant P(this); Cách viết thứ 2 sẽ làm cho điều kiện sau dễ chứng minh ở hàm khởi tạo. Nguyễn Thị Minh Tuyền 20 Đặc tả hình thức
21. Các giả sử trái ngược nhau v Nếu ta đặc tả trái ngược nhau thì ta chứng minh gì cũng đúng. public class Inconsistent { public void m() { int a,b,c,d; //@ assume a == b; //@ assume b == c; //@ assume a != c; //@ assert a == d; // Passes, but inconsistent //@ assert false; // Passes, but inconsistent } } Nguyễn Thị Minh Tuyền 21 Đặc tả hình thức
22. v Một ví dụ khác: public class Inconsistent2 { public int a,b,c,d; //@ invariant a == b; //@ invariant b == c; //@ invariant a != c; public void m() { //@ assert a == d; // Passes, but inconsistent //@ assert false; // Passes, but inconsistent } } Nguyễn Thị Minh Tuyền 22 Đặc tả hình thức
23. Exposed references v Vấn đề có thể phát sinh khi tham chiếu đến một đối tượng bên trong được export từ một lớp: public class Exposed { /*@ non_null */ private int[] a = new int[10]; //@ invariant a.length > 0 && a[0] >= 0; //@ ensures \result != null; //@ ensures \result.length > 0; //@ pure public int[] getArray() { return a; } } class X { void m(/*@ non_null */ Exposed e) { e.getArray()[0] = -1; // unchecked invariant violation } } § ESC/Java không kiểm tra rằng mọi đối tượng được cấp phát bộ nhớ vẫn thỏa mãn các bất biến của nó. § Các vấn đề tương tự có thể giải quyết nếu các trường public được thay đổi trực tiếp. Nguyễn Thị Minh Tuyền 23 Đặc tả hình thức
24. Nội dung 1. Đặc tả thừa kế 2. Aliasing 3. Object invariants 4. Giả thuyết không nhất quán 5. Exposed references 6. \old 7. Viết đặc tả thế nào Nguyễn Thị Minh Tuyền 24 Đặc tả hình thức
25. \old v \old được dùng để chỉ giá trị ở trạng thái trước trong một biểu thức điều kiện sau. v Xem xét đặc tả § public static native void arraycopy(Object[] src, int srcPos, Object[] dest, int destPos, int length); v Thử: § ensures (\forall int i; 0<=i && i<length; dest[destPos +i] == src[srcPos+i]); Sai! § ensures (\forall int i; 0<=i && i<length; dest[destPos +i] == \old(src[srcPos+i]); Nguyễn Thị Minh Tuyền 25 Đặc tả hình thức
26. v Trong điều kiện sau: § ensures (\forall int i; 0<=i && i<length; dest[destPos+i] == \old (src[srcPos+i]); § public static native void arraycopy(Object[] src, int srcPos, Object[] dest, int destPos, int length); v Tại sao ta không viết \old(length) thay vì length? v Và \old(dest)[ ] thay vì dest[ ]? v Bất cứ một tham số x nào trong điều kiện sau đều có nghĩa là \old(x). v Điều này nghĩa là không thể chỉ đến giá trị mới của length trong điều kiện sau của arraycopy.Nhưng giá trị này không thấy bởi client. Nguyễn Thị Minh Tuyền 26 Đặc tả hình thức
27. Nội dung 1. Đặc tả thừa kế 2. Aliasing 3. Object invariants 4. Giả thuyết không nhất quán 5. Exposed references 6. \old 7. Viết đặc tả thế nào Nguyễn Thị Minh Tuyền 27 Đặc tả hình thức
28. v Đối với mỗi trường: § có bất biến nào cho trường này không? v Đối với mỗi tham chiếu trường: § có nên thêm non_null không? § có nên có một trường owner để thiết lập cho nó hay không? v Đối với mỗi phương thức? § phương thức đó có nên là pure hay không? các tham số và kết quả có nên non_null hay không? v Đối với mỗi lớp: bất biến nào thể hiện tính nhất quán của dữ liệu bên trong? v Thêm điều kiện trước và điều kiện sau đề giới hạn đầu vào và đầu ra của mỗi phương thức. v Thêm các ngoại lệ không được kiểm tra cho các mệnh đề throws. v Bắt đầu với các đặc tả đơn giản, thực hiện phức tạp dần lên khi chúng có giá trị. Nguyễn Thị Minh Tuyền 28 Đặc tả hình thức
29. v Tách rời các phép nối để lấy thông tin về các phép nối bị vi phạm. Sử dụng requires A; requires B; và không dùng requires A && B; v Sử dụng các phát biểu assert để tìm ra cái gì đang bị sai. v Sử dụng assume về điều bạn biết là đúng để hỗ trợ cho việc chứng minh. Nguyễn Thị Minh Tuyền 29 Đặc tả hình thức