Đặ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

LOGO Đặc tả hình thức Nguyễn Thị Minh Tuyền 1 Giới thiệu về ESC/Java2 Thủ thuật và cạm bẫy 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 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 2 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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 3 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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. 4 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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ó. 5 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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. 6 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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. 7 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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ì? 8 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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){ ... } } 9 Nguyễn Thị Minh Tuyền Đặc tả hình thức Đặ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); } 10 Nguyễn Thị Minh Tuyền Đúng cho tất cả các Object Không nhất thiết đúng cho tất cả các subtype Đặc tả hình thức Đặ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. 11 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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 12 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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<=i && i < a.length; public void insert(int i, int v) { a[i] = v; if (v < 0) noneg = false; } } tạo ra Alias.java:12: Warning: Possible violation of object invariant (Invariant) }ˆ Associated declaration is “Alias.java", line 5, col 6: /*@ invariant noneg ==> (\forall int i; 0<=i && i <a.length; ... 13 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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. 14 Nguyễn Thị Minh Tuyền int noneg int[] a this brokenObj int noneg int[] a một đối tượng int[] Đặc tả hình thức 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; //@ requires 0<=i && i < a.length; public void insert(int i, int v) { a[i] = v; if (v < 0) noneg = false; } public Alias() { //@ set a.owner = this; } } 15 Nguyễn Thị Minh Tuyền this int noneg int[] a brokenObj int noneg int[] a một đối tượng int[] int[] .... owner một đối tượng int[] int[] .... owner Đặc tả hình thức 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(); } 16 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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. 17 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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. 18 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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 19 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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. 20 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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 } } 21 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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 } } 22 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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. 23 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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 24 Nguyễn Thị Minh Tuyền Đặc tả hình thức \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]); 25 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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. 26 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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 27 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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ị. 28 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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. 29 Nguyễn Thị Minh Tuyền