Bài giảng Đặc tả hình thức: Chương 10 - Nguyễn Thị Minh Tuyền

LOGO<br /> <br /> Đặc tả hình thức<br /> Giới thiệu về Java Modeling Language<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 1<br /> <br /> Nội dung<br /> v Giới thiệu về JML<br /> v Công cụ hỗ trợ cho JML<br /> v ESC/Java2: Cách sử dụng và thuộc<br /> tính<br /> v ESC/Java2: các cảnh báo<br /> v Một số chỉ dẫn về đặc tả và điểm yếu<br /> v JML nâng cao<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 2<br /> <br /> Đặc tả hình thức<br /> <br /> Java Modeling Language<br /> v  Java Modeling Language (JML)<br /> §  http://www.eecs.ucf.edu/~leavens/JML/index.shtml<br /> <br /> v  Tài liệu:<br /> §  http://www.kindsoftware.com/products/opensource/ESCJava2/<br /> docs.html<br /> <br /> v  Ngôn ngữ đặc tả hình thức cho Java<br /> §  đặc tả hành vi của các lớp trong Java<br /> §  ghi lại các quyết định về thiết kế và cài đặt<br /> bằng cách thêm vào trong mã nguồn Java các assertion<br /> §  điều kiện trước (pre-condition)<br /> §  điều kiện sau (post-condition)<br /> §  bất biến (invariant)<br /> v  Mục tiêu: người lập trình Java nào cũng có thể<br /> sử dụng dễ dàng.<br /> Nguyễn Thị Minh Tuyền<br /> <br /> 3<br /> <br /> Đặc tả hình thức<br /> <br /> v JML assertion được thêm vào dưới<br /> dạng các chú thích trong file .java<br /> §  /*@ ... @*/ hoặc //@<br /> <br /> v Các thuộc tính được đặc tả dưới dạng<br /> các biểu thức boolean và được mở<br /> rộng với một số toán tử (\old, \forall,<br /> \result, ...).<br /> v sử dụng một số từ khóa ( requires,<br /> ensures, signals, assignable, pure,<br /> invariant, non_null, ...)<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 4<br /> <br /> Đặc tả hình thức<br /> <br /> Điều kiện trước và sau<br /> (pre- và post-condition)<br /> v Điều kiện trước của một phương thức<br /> là điều kiện phải đúng trước khi gọi<br /> phương thức đó.<br /> §  Sử dụng từ khóa requires.<br /> <br /> v Điều kiện sau của một phương thức là<br /> điều kiện phải đúng khi nó kết thúc.<br /> §  Điều kiện sau bình thường đặc tả cái gì phải đúng khi<br /> phương thức trả về bình thường, nghĩa là không có<br /> ngoại lệ. Sử dụng từ khóa ensures.<br /> §  Điều kiện sau đặc tả những gì xảy ra khi có ngoại lệ.<br /> Sử dụng từ khóa signals.<br /> Nguyễn Thị Minh Tuyền<br /> <br /> 5<br /> <br /> Đặc tả hình thức<br /> <br />