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)
§ http://www.eecs.ucf.edu/~leavens/JML/index.shtml
v Tài liệu:
§ http://www.kindsoftware.com/products/opensource/ESCJava2/
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