Đặc tả hình thức - Giới thiệu về ESC/Java2 Cách sử dụng và thuộc tính - 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 Cách sử dụng và thuộc tính 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 ESC/Java §  Extended Static Checker for Java 2 Nguyễn Thị Minh Tuyền Đặc tả hình thức Cấu trúc của ESC/Java2 v ESC/Java2 gồm §  Một pha kiểm tra cú pháp §  Một pha typechecking (kiểm tra loại và cách sử dụng) §  Một pha kiểm tra tĩnh ( diễn giải để tìm ra các lỗi tìm tàng) – chạy một prover behind-the-scenes gọi là Simplify. v Kiểm tra cú pháp và typechecking tạo ra các cảnh báo hoặc lỗi. v Kiểm tra tĩnh đưa ra các cảnh báo. 3 Nguyễn Thị Minh Tuyền Đặc tả hình thức Chạy ESC/Java2 v Tải ESC/Java2 từ §  ESCJava2/download.html v Sử dụng ESC/Java2: §  Chạy công cụ bằng lệnh. §  Sử dụng Eclipse plug-in. §  Hướng dẫn cài đặt: ESCJava2/ 4 Nguyễn Thị Minh Tuyền Đặc tả hình thức Platform được hỗ trợ v ESC/Java2 được hỗ trợ trên §  Linux §  MacOSX §  Cygwin on Windows §  Windows (nhưng vẫn còn một số vấn đề về môi trường cần được giải quyết) §  Solaris 5 Nguyễn Thị Minh Tuyền Đặc tả hình thức Môi trường v Ứng dụng dựa vào môi trường có §  Một prover Simplify chạy được trên môi trường sử dụng ESC/Java2, thường là cùng đường dẫn với file jar của ứng dụng. §  Biến môi trường SIMPLIFY thiết lập tên của file thực thi cho môi trường này. §  Tập các đặc tả cho các file hệ thống Java, mặc định được bundle vào trong file jar của ứng dụng, nhưng cũng nằm trong jmlspecs.jar. §  Các script cần biến môi trường ESCTOOLS_RELEASE được thiết lập tới đường dẫn chứa bản release. 6 Nguyễn Thị Minh Tuyền Đặc tả hình thức Các tùy chọn dòng lệnh v  Một số thông số trên dòng lệnh là tùy chọn hoặc các tham số hoặc là đầu vào. Các tùy chọn thông dụng nhất được sử dụng là: §  -help - prints a usage message §  -quiet - turns off informational messages (e.g. progress messages) §  -nowarn - turns off a warning §  -classpath - sets the path to find referenced classes [best if it contains ‘.’] §  -specs - sets the path to library specification files §  -simplify - provides the path to the simplify executable §  -f - the argument is a file containing command-line arguments §  -nocheck - parse and typecheck but no verification §  -routine - restricts checking to a single routine §  -eajava, -eajml - enables checking of Java assertions §  -counterexample - gives detailed information about a warning 7 Nguyễn Thị Minh Tuyền Đặc tả hình thức Đầu vào v Đầu vào trên dòng lệnh là các lớp được kiểm tra. Nhiều lớp khác có thể được tham chiếu cho các định nghĩa lớp hoặc các đặc tả - những lớp này được tìm thấy trong classpath (hoặc sourcepath hoặc specspath). §  file names: file java hoặc file đặc tả (tương đối với đường dẫn hiện tại). §  directories: xử lý tất cả các file java và đặc tả (tương đối với đường dẫn hiện tại) §  package: được tìm thấy trong classpath §  class: được tìm thấy trong classpath §  list (mở đầu bằng –list): một file chứa các đầu vào 8 Nguyễn Thị Minh Tuyền Đặc tả hình thức Các file đặc tả v Đặc tả có thể được thêm trực tiếp vào các file .java v Đặc tả có thể được thêm vào trong các file đặc tả §  Không có cài đặt của phương thức §  Không có khởi tạo field §  Hậu tố bắt buộc: .refines-java §  Yêu cầu một annotation refines §  Cũng phải nằm trong classpath 9 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ về file đặc tả package java.lang; import java.lang.reflect.*; import java.io.InputStream; public final class Class implements java.io.Serializable { private Class(); /*@ also public normal_behavior @ ensures \result != null && !\result.equals("") @ && (* \result is the name of this class object *); @*/ public /*@ pure @*/ String toString(); .... 10 Nguyễn Thị Minh Tuyền Đặc tả hình thức Demo v Ví dụ Bag 11 Nguyễn Thị Minh Tuyền Đặc tả hình thức modular reasoning v ESC/Java2 suy luận về từng phương thức đơn lẻ. Vì thế, trong class A{ byte[] b; public void n() { b = new byte[20]; } public void m() { n(); b[0] = 2; ... } v ESC/Java2 cảnh báo rằng có thể có một dereference null ở đây, thậm chí ta có thể thấy rằng điều đó không xảy ra. 12 Nguyễn Thị Minh Tuyền Đặc tả hình thức modular reasoning v Để dừng cảnh bảo của ESC/Java2 : thêm một điều kiện sau class A{ byte[] b; //@ ensures b != null && b.length = 20; public void n() { b = new byte[20]; } public void m() { n(); b[0] = 2; ... } v Vì vậy: thuộc tính liên quan của phương thức phải được chỉ ra rõ ràng. v Các lớp con override các phương thức phải bảo toàn những điều này. 13 Nguyễn Thị Minh Tuyền Đặc tả hình thức modular reasoning v Tương tự, ESC/Java2 sẽ cảnh báo về b[0]=2 trong class A{ byte[] b; public void A() { b = new byte[20]; } public void m() { b[0] = 2; ... } v Có thể ta thấy có một cảnh báo giả mạo, dù điều này có thể khó hơn trong ví dụ trước: ta sẽ phải xem xét tất cả các khởi tạo và tất cả các phương thức. 14 Nguyễn Thị Minh Tuyền Đặc tả hình thức modular reasoning v Để không còn cảnh báo ESC/Java2: ta thêm một bất biến class A{ byte[] b; //@ invariant b != null && b.length == 20; // or weaker property for b.length ? public void A() { b = new byte[20]; } public void m() { b[0] = 2; ... } v Vì vậy: các thuộc tính liên quan phải được chỉ rõ. v Các lớp con phải bảo toàn các thuộc tính này. 15 Nguyễn Thị Minh Tuyền Đặc tả hình thức assume v Thay vì dừng cảnh báo ESC/Java2: thêm một giả định: ... //@ assume b != null && b.length > 0; b[0] = 2; ... v Đặc biệt hữu ích trong quá trình phát triển, khi ta vẫn còn đang cố gắng tìm ra các giả định bị che lấp, hoặc khi độ mạnh để suy diễn của ESC/ Java2 quá yếu. v (requires có thể được hiểu như một hình thức của assume). 16 Nguyễn Thị Minh Tuyền Đặc tả hình thức cần có các mệnh đề assignable class A{ byte[] b; ... public void m() { ... b = new byte[3]; //@ assert b[0] == 0; // ok! o.n(...); //@ assert b[0] == 0; // ok? ... } v ESC/Java cần biết gì về o.n để kiểm tra assert thứ hai? 17 Nguyễn Thị Minh Tuyền Đặc tả hình thức cần có các mệnh đề assignable class A{ byte[] b; ... public void m() { ... b = new byte[3]; //@ assert b[0] == 0; // ok! o.n(b); //@ assert b[0] == 0; // ok? ... } v Một đặc tả chi tiết cho o.n có thể đặt trong điều kiện sau rằng b[0] vẫn là 0. 18 Nguyễn Thị Minh Tuyền Đặc tả hình thức cần có các mệnh đề assignable class A{ byte[] b; ... public void m() { ... b = new byte[3]; //@ assert b[0] == 0; // ok! o.n(); //@ assert b[0] == 0; // ok? ... } §  Nếu điều kiện sau của o.n không cho ta biết b không null – và không thể mong đợi điều đó – ta cần mệnh đề assignable để nói rằng o.n sẽ không ảnh hưởng b[0]. §  Khai báo o.n như một pure sẽ giải quyết được vấn đề. 19 Nguyễn Thị Minh Tuyền LOGO