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

LOGO

Đặc tả hình thức
Giới thiệu về Java Modeling Language

Nguyễn Thị Minh Tuyền

Nguyễn Thị Minh Tuyền

1

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

Nguyễn Thị Minh Tuyền

2

Đặ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.
Nguyễn Thị Minh Tuyền

3

Đặ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, ...)

Nguyễn Thị Minh Tuyền

4

Đặ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.
Nguyễn Thị Minh Tuyền

5

Đặc tả hình thức