Đặc tả hình thức - JML nâng cao P2 - 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 v Aliasing 2 Nguyễn Thị Minh Tuyền Đặc tả hình thức Aliasing v Aliasing là nguồn gốc của mọi rắc rối phức tạp. v Lớp ArrayTimer minh họa cho điều này. 3 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ ArrayTimer v Sử dụng một mảng 6 số để biểu diễn giờ:phút:giây public class ArrayTimer{ char[] currentTime; char[] alarmTime; //@ invariant currentTime != null; //@ invariant currentTime.length == 6; //@ invariant alarmTime != null; //@ invariant alarmTime.length == 6; public void tick() { ... } public void setAlarm(...) { ... } } 4 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ ArrayTimer v Sẽ sai nếu các instance khác nhau của ArrayTimer cùng chia sẻ mảng alarmTime, nghĩa là §  o.alarmTime == o’.alarmTime §  cho o !=o’ §  ESC/Java2 có thể chú ý đến điều này, sinh ra một cảnh báo đúng nhưng khó hiểu. 5 Nguyễn Thị Minh Tuyền Đặc tả hình thức v Để loại bỏ aliasing của các trường alarmTime: public class ArrayTimer{ char[] currentTime; //@ invariant currentTime.owner == this; ... public ArrayTimer( ...){ ...; currentTime = new char[6]; //@ set currentTime.owner = this; ... } } 6 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ ArrayTimer v Sẽ sai nếu một instance của ArrayTimer định danh alarmTime của nó thành currentTime của nó, nghĩa là o.alarmTime == o.currentTime v ESC/Java2 có thể để ý điều này, sinh ra một cảnh báo đúng nhưng khó hiểu. v Ta nên thêm //@ invariant alarmTime != currentTime; để loại bỏ các alias như vậy. 7 Nguyễn Thị Minh Tuyền Đặc tả hình thức v Các trường chỉ sử dụng ở mức đặc tả: trường ghost và model 8 Nguyễn Thị Minh Tuyền Đặc tả hình thức Trường Ghost v Đôi khi sẽ thuận tiện nếu ta thêm một trường mở rộng, chỉ phục vụ cho mục đích của đặc tả (gọi là biến phụ). v Một trường ghost giống một trường bình thường, ngoại trừ nó chỉ được dùng trong đặc tả. v Một lệnh đặc biệt set có thể được dùng để gán một giá trị cho một trường ghost. 9 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ v Giả sử trong đặc tả không hình thức class SimpleProtocol { public void start() { ... } public void stop() { ... } } v nói rằng stop() chỉ có thể được triệu gọi sau start(), và ngược lại. v Điều này có thể được biểu diễn sử dụng trường ghost, để biểu diễn trạng thái của protocol. 10 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ class SimpleProtocol { //@ public ghost boolean started; //@ requires !started; //@ assignable started; //@ ensures started; public void start() { ... //@ set started = true; } //@ requires started; //@ assignable started; //@ ensures !started; public void stop() { ... //@ set started = false; } } 11 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ v Có thể đối tượng có cùng trạng thái bên trong mà nó ghi lại nếu protocol đang thực thi, ví dụ: class SimpleProtocol { private /*@ spec_public*/ ProtocolStack st; ... public void start() { ... st = new ProtocolStack(...); ... } public void stop() { ... st = null; ... } } 12 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ v Có thể biểu diễn quan hệ giữa các trường ghost và một số trường khác. Ví dụ: class SimpleProtocol { private ProtocolStack st; //@ public ghost boolean started; //@ invariant started (st !=null); //@ requires !started; //@ assignable started; //@ ensures started; public void start() { ... } //@ requires started; //@ assignable started; //@ ensures !started; public void stop() { ... } } 13 Nguyễn Thị Minh Tuyền Đặc tả hình thức v  Ta có thể không dùng trường ghost, và sử dụng: class SimpleProtocol { private /*@ spec_public @*/ ProtocolStack st; //@ requires st==null; //@ assignable st; //@ ensures st!=null; public void start() { ... } //@ requires st!=null; //@ assignable st; //@ ensures st==null; public void stop() { ... } } v  nhưng cách này không đẹp mắt và làm lộ rõ các chi tiết cài đặt. 14 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ: các trường model v Giải pháp: sử dụng một trường model class SimpleProtocol { private ProtocolStack st; //@ public model boolean started; //@ private represents started = (st != null); //@ requires !started; //@ assignable started; //@ ensures started; public void start() { ... } //@ requires started; //@ assignable started; //@ ensures !started; public void stop() { ... } } 15 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ: các trường model v Một trường model cũng cung cấp một nhóm dữ liệu có liên quan class SimpleProtocol { private ProtocolStack st; //@ in started; //@ public model boolean started; //@ private represents started = (st != null); //@ requires !started; //@ assignable started; //@ ensures started; public void start() { ... } //@ requires started; //@ assignable started; //@ ensures !started; public void stop() { ... } } 16 Nguyễn Thị Minh Tuyền Đặc tả hình thức model vs. ghost v Sự khác nhau giữa ghost và model có thể dễ gây nhầm lẫn. Cả hai đều tồn tại trong đặc tả JML, không phải trong mã nguồn. v Ghost §  Trường ghost giống một trường bình thường §  Ta có thể gán giá trị cho nó, sử dụng set, trong đặc tả JML. v Model §  Trường model là một trường trừu tượng. §  Trường model là một cách viết tắt thuận tiện. §  Ta không thể gán giá trị cho nó. §  Trường model thay đổi giá trị của nó khi việc biểu diễn thay đổi. 17 Nguyễn Thị Minh Tuyền Đặc tả hình thức v Bất biến (invariant) 18 Nguyễn Thị Minh Tuyền Đặc tả hình thức Bất biến v Bất biến – còn gọi là bất biến lớp – là khái niệm phổ biến và hữu ích. v Trong các chương trình lớn hơn, chỉ những ràng buộc thật quan trọng được đặc tả sử dụng bất biến. v Tuy nhiên, ngữ nghĩa phức tạp hơn mong đợi rất nhiều. v Bất biến gồm điều kiện trước và điều kiện sau của phương thức, và trong điều kiện sau của một phương thức khởi tạo. Và còn nhiều hơn thế nữa ... 19 Nguyễn Thị Minh Tuyền Đặc tả hình thức Khi nào một bất biến nên đúng public class A { B b; int i=2; //@ invariant i >= 0 //@ ensures \result >=0; public /*@ pure @*/int get(){ return i; } public void m(){ i--; ... ; i++; } } v Một bất biến có thể tạm thời bị phá vỡ. 20 Nguyễn Thị Minh Tuyền // invariant possibly broken Đặc tả hình thức Khi nào một bất biến nên đúng public class A { B b; int i=2; //@ invariant i >= 0 //@ ensures \result >=0; public /*@ pure @*/ int get(){ return i; } public void m(){ i--; b.m(...); i++; } } v Có thể sinh ra vấn đề nếu triệu gọi b.m gồm việc triệu gọi đối tượng hiện tại. 21 Nguyễn Thị Minh Tuyền // invariant possibly broken Đặc tả hình thức Khi nào một bất biến nên đúng v Ví dụ, giả sử public class B { ... public void m(A a){ ... int j = a.get(); //@ assert i>=0; ... } } v Đặc tả của get() giả sử rằng assertion sẽ đúng. v  Nhưng nếu get() được triệu gọi khi một bất biến bị phá vỡ, tất cả sẽ không còn đúng nữa. v Điều này gọi là vấn đề call-back. 22 Nguyễn Thị Minh Tuyền Đặc tả hình thức Khi nào một bất biến nên đúng v Giải pháp cho vấn đề call-back: §  Một bất biến phương thức nên đúng trong tất cả các trạng thái thấy được, tất cả trạng thái từ đầu đến cuối của việc triệu gọi phương thức. v Vì vậy bất biến có nhiều vấn đề khác chứ không chỉ thêm chúng vào điều kiện trước và điều kiện sau. v Tất cả các bất biến của tất cả các đối tượng nên đúng trong các trạng thái thấy được. v ESC/Java2 tìm kiếm chỉ tại bất biến của một số đối tượng. v Các kỹ thuật kiểm định mô đun hóa là một thử thách, vẫn còn là đề tài nóng trong nghiên cứu. 23 Nguyễn Thị Minh Tuyền Đặc tả hình thức Khi nào một bất biến nên đúng v Đôi khi ta muốn triệu gọi một phương thức tại một điểm của chương trình nơi mà bất biến bị phá vỡ. Để làm điều này mà không bị ESC/Java2 than phiền: §  Khai báo một phương thức private như là một phương thức helper. private /*@ helper @*/ void m() { ... } Bất biến không phải đúng khi một phương thức helper như vậy được gọi. §  Thêm //@ nowarn Invariant §  trong dòng tại đó việc gọi phương thức này xảy ra. Điều này không an toàn. 24 Nguyễn Thị Minh Tuyền Đặc tả hình thức Nhiều vấn đề với bất biến public class SortedLinkedList { private int i; private LinkedList next; //@ invariant i > next.i; public /*@ pure @*/ int getValue(){ return i; } public /*@ pure @*/ int getNext(){ return next; } public /*@ pure @*/ int getValue(){ return i; } public void inc() { i++; } } v inc sẽ không phá vỡ bất biến đối tượng này, nhưng có thể phá vỡ bất biến của đối tượng xem đối tượng này như đối tượng next của nó. 25 Nguyễn Thị Minh Tuyền