Đặc tả hình thức - Giới thiệu về Java Modeling Language - Nguyễn Thị Minh Tuyền

LOGO Đặc tả hình thức Nguyễn Thị Minh Tuyền Nguyễn Thị Minh Tuyền 1 Giới thiệu về Java Modeling Language Đặc tả hình thức Nội dung v Giới thiệu về JML v Công cụ hỗ trợ cho JML v ESC/Java2: Cách sử dụng và thuộc tính v ESC/Java2: các cảnh báo v Một số chỉ dẫn về đặc tả và điểm yếu v JML nâng cao 2 Nguyễn Thị Minh Tuyền Đặc tả hình thức Java Modeling Language v  Java Modeling Language (JML) §  v  Tài liệu: §  docs.html v  Ngôn ngữ đặc tả hình thức cho Java §  đặc tả hành vi của các lớp trong Java §  ghi lại các quyết định về thiết kế và cài đặt bằng cách thêm vào trong mã nguồn Java các assertion §  điều kiện trước (pre-condition) §  điều kiện sau (post-condition) §  bất biến (invariant) v  Mục tiêu: người lập trình Java nào cũng có thể sử dụng dễ dàng. 3 Nguyễn Thị Minh Tuyền Đặc tả hình thức v JML assertion được thêm vào dưới dạng các chú thích trong file .java §  /*@ ... @*/ hoặc //@ v Các thuộc tính được đặc tả dưới dạng các biểu thức boolean và được mở rộng với một số toán tử (\old, \forall, \result, ...). v sử dụng một số từ khóa ( requires, ensures, signals, assignable, pure, invariant, non_null, ...) 4 Nguyễn Thị Minh Tuyền Đặc tả hình thức Điều kiện trước và sau (pre- và post-condition) v Điều kiện trước của một phương thức là điều kiện phải đúng trước khi gọi phương thức đó. §  Sử dụng từ khóa requires. v Điều kiện sau của một phương thức là điều kiện phải đúng khi nó kết thúc. §  Điều kiện sau bình thường đặc tả cái gì phải đúng khi phương thức trả về bình thường, nghĩa là không có ngoại lệ. Sử dụng từ khóa ensures. §  Điều kiện sau đặc tả những gì xảy ra khi có ngoại lệ. Sử dụng từ khóa signals. 5 Nguyễn Thị Minh Tuyền Đặc tả hình thức requires, ensures v Điều kiện trước và sau cho phương thức có thể được đặc tả. /*@ requires amount >= 0; ensures balance == \old(balance)-amount && \result == balance; @*/ public int debit(int amount) { ... } v Ở đây, \old(balance) chỉ đến giá trị của balance trước khi thực thi phương thức debit(int amount). 6 Nguyễn Thị Minh Tuyền Đặc tả hình thức requires, ensures v Các đặc tả JML có thể mạnh yếu tùy vào cách đặc tả /*@ requires amount >= 0; ensures true; @*/ public int debit(int amount) { ... Điều kiện sau mặc định “ensures true” có thể được bỏ qua. 7 Nguyễn Thị Minh Tuyền Đặc tả hình thức Design-by-Contract v Điều kiện trước và sau định nghĩa ràng buộc (contract) giữa một lớp và client của nó. §  Client phải đảm bảo điều kiện trước và có thể giả định điều kiện sau. §  Phương thức có thể giả định điều kiện trước và phải đảm bảo điều kiện sau. v Ví dụ: §  trong ví dụ về phương thức debit, obligation của client là đảm bảo rằng giá trị của amount dương. Mệnh đề requires phải làm rõ ràng điều này. 8 Nguyễn Thị Minh Tuyền Đặc tả hình thức signals v Điều kiện sau cho ngoại lệ có thể được đặc tả sử dụng signals. /*@ requires amount >= 0; ensures true; signals (BankException e) && amount > balance && balance == \old(balance) && e.getReason().equals("Amount too big"); @*/ public int debit(int amount) throws BankException ... } 9 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ý nghĩa của điều kiện sau ensures .... normal (return) signals () .... exceptional (throw) Đặc tả hình thức v Các ngoại lệ được đề cập trong mệnh đề throws mặc định được cho phép. Để thay đổi điều này, có 3 tùy chọn: §  Loại trừ các ngoại lệ, sử dụng normal_behavior /*@ normal_behavior requires ... ensures ... @*/ §  Để loại trừ một số ngoại lệ E, thêm signals (E) false; §  Để cho phép một số ngoại lệ, thêm signals_only E1, ..., E2; 11 Nguyễn Thị Minh Tuyền Đặc tả hình thức Bất biến v Các bất biến (invariant) là các thuộc tính phải được duy trì trong tất cả các phương thức. public class Wallet { public static final short MAX_BAL = 1000; private short balance; /*@ invariant 0 <= balance && balance <= MAX_BAL; @*/ ... v Bất biến có trong tất cả các điều kiện trước và sau. Bất biết cũng phải được bảo toàn nếu có ngoại lệ. 12 Nguyễn Thị Minh Tuyền Đặc tả hình thức Bất biến v Bất biến có thể là tài liệu về các quyết định thiết kế. public class Directory { private File[] files; /*@ invariant files != null && (\forall int i; 0 <= i && i < files.length; ; files[i] != null && files[i].getParent() == this); @*/ .... } v Nếu bất biến được đặc tả rõ ràng, nó sẽ hỗ trợ cho việc hiểu rõ mã nguồn. 13 Nguyễn Thị Minh Tuyền Đặc tả hình thức non_null v Nhiều bất biến, điều kiện trước và sau là các tham chiếu không null. Sử dụng non_null là cách đơn giản để đặc tả điều này. public class Directory { private /*@ non_null @*/ File[] files; void createSubdir(/*@ non_null @*/ String name){ ... /*@ non_null @*/ Directory getParent(){ ... 14 Nguyễn Thị Minh Tuyền Đặc tả hình thức assert v Mệnh đề assert đặc tả một thuộc tính phải đúng tại một điểm trong mã nguồn. if (i <= 0 || j < 0) { ... } else if (j < 5) { //@ assert i > 0 && 0 < j && j < 5; ... } else { //@ assert i > 0 && j > 5; ... } 15 Nguyễn Thị Minh Tuyền Đặc tả hình thức assert v Từ khóa assert cũng có trong Java (từ phiên bản Java 1.4). Tuy nhiên, assert trong JML giàu ngữ nghĩa hơn. ... for (n = 0; n < a.length; n++) if (a[n]==null) break; /*@ assert (\forall int i; 0 <= i && i < n; a[i] != null); @*/ 16 Nguyễn Thị Minh Tuyền Đặc tả hình thức assignable /*@ requires amount >= 0; assignable balance; ensures balance == \old(balance)-amount; @*/ public int debit(int amount) { } ... Mệnh đề assignable mặc định: assignable \everything 17 Nguyễn Thị Minh Tuyền Đặc tả hình thức pure v Một phương thức mà không có hiệu ứng phụ gọi là pure. public /*@ pure @*/ int getBalance(){... Directory /*@ pure non_null @*/ getParent(){...} v Phương thức pure chỉ ra rằng assignable \nothing. 18 Nguyễn Thị Minh Tuyền Đặc tả hình thức Từ khóa trong JML v Một số từ khóa trong JML đã sử dụng: §  requires §  ensures §  signals §  assignable §  normal_behavior §  invariant §  non_null §  pure §  \old, \forall, \exists, \result 19 Nguyễn Thị Minh Tuyền Đặc tả hình thức v Công cụ cho JML 20 Nguyễn Thị Minh Tuyền Đặc tả hình thức Các công cụ cho JML v Phân tích cú pháp và typechecking v Kiểm tra assertion tại thời gian thực thi (runtime assertion checking): §  Kiểm thử các vi phạm của các assertion trong khi chạy chương trình. §  jmlrac v Kiểm định chương trình tự động: §  Chứng minh rằng các ràng buộc không bao giờ bị vi pham tại thời điểm biên dịch. §  ESC/Java2 §  Đây là kiểm chứng chương trình, không chỉ là kiểm thử. 21 Nguyễn Thị Minh Tuyền Đặc tả hình thức Kiểm tra assertion tại thời gian thực thi v Trình biên dịch jmlrac được viết bởi Gary Leavens, Yoonsik Cheon và các cộng sự tại Iowa State University. §  Chuyển các assertion JML thành các runtime check: trong khi thực thi, tất cả các assertion được kiểm tra và bất kỳ vi phạm nào của assertion đều sinh ra một lỗi. §  Thực hiện đơn giản như là một phần của các nguyên tắc kiểm thử hiện có. §  Kiểm thử tốt hơn và phản hồi tốt hơn, vì nhiều thuộc tính được kiểm tra, tại nhiều vị trí trong mã nguồn. 22 Nguyễn Thị Minh Tuyền Đặc tả hình thức Kiểm tra assertion tại thời gian thực thi v jmlrac có thể phát sinh các mã kiểm tra phức tạp. Ví dụ: /*@ ... signals (Exception) balance == \old(balance); @*/ public int debit(int amount) { ... } v Kiểm tra rằng nếu debit throws một ngoại lệ, balance không thay đổi và bất biến vẫn đúng. 23 Nguyễn Thị Minh Tuyền Đặc tả hình thức Kiểm tra tĩnh mở rộng v ESC/Java(2) §  Kiểm tra tĩnh mở rộng(extended static checking) = kiểm thử chương trình tự động một cách đầy đủ, với một số thỏa hiệp để đạt được sự tự động một cách đầy đủ. §  Cố gắng chứng minh tính đúng đắn của đặc tả tại thời điểm biên dịch, hoàn toàn tự động. §  ESC/Java có thể bỏ qua một lỗi đang tồn tại. §  ESC/Java có thể cảnh báo các lỗi không xảy ra. §  Nhưng tìm được nhiều bug tìm tàng một cách nhanh chóng. §  Chứng minh sự vắng mặt của các ngoại lệ thời gian thực thi rất tốt (ví dụ như Null-, ArrayIndexOutOfBounds-, ClassCast-) và kiểm tra một số thuộc tính đơn giản. 24 Nguyễn Thị Minh Tuyền Đặc tả hình thức v  ESC/Java có thể thất bại trong việc tạo ra các cảnh báo về chương trình không đúng. v  Ví dụ: public class Positive{ private int n = 1; //@ invariant n > 0; public void increase(){ n++; } } v  ESC/Java 2 không tạo ra cảnh báo nào, nhưng hàm increase sẽ phá vỡ điều kiện trong bất biến, chẳng hạn với n = 232 - 1 25 Nguyễn Thị Minh Tuyền Đặc tả hình thức Kiểm tra tĩnh và kiểm tra tại thời gian thực thi v  Điểm khác nhau quan trọng: §  ESC/Java2 kiểm tra đặc tả tại thời điểm biên dịch, jmlrac kiểm tra đặc tả tại thời điểm thực thi §  ESC/Java2 chứng minh tính đúng đắn của đặc tả, jml chỉ kiểm thử tính đúng đắng của đặc tả. Vì vậy: •  ESC/Java2 không phụ thuộc vào bộ test nào, kết quả kiểm thử tại thời gian thực thi chỉ đúng với bộ test, •  ESC/Java2 cung cấp mức độ cao hơn về độ tin tưởng. v  Để đạt được điều này: ta phải đặc tả tất cả điều kiện trước và sau của các phương thức và các bất biến cần thiết cho việc kiểm định. 26 Nguyễn Thị Minh Tuyền Đặc tả hình thức Các công cụ JML khác v  Tài liệu theo kiểu javadoc: jmldoc v  Eclipse plugin v  Một số công cụ kiểm định đầy đủ: §  LOOP tool + PVS (Nijmegen) §  JACK (Gemplus/INRIA) §  Krakatoa tool + Coq (INRIA) §  KeY (Chalmers + Germany) v  Những công cụ này cũng cho phép kiểm định tương tác (trong khi ESC/Java2 chỉ nhắm đến việc kiểm định hoàn toàn tự động) và vì vậy có thể chứng minh các thuộc tính phức tạp. v  runtime detection of invariants: Daikon (Michael Ernst,MIT) v  model-checking multi-threaded programs: Bogor(Kansas State) 27 Nguyễn Thị Minh Tuyền LOGO