LOGO
Đặc t hình thc
Nguyn Th Minh Tuyn
Nguyn Th Minh Tuyn 1
Gii thiu v Java Modeling Language
Đặc t hình thc
Ni dung
vGii thiu v JML
vCông c h tr cho JML
vESC/Java2: Cách s dng và thuc
tính
vESC/Java2: các cnh báo
vMt s ch dn v đặc tđim yếu
vJML nâng cao
2
Nguyn Th Minh Tuyn
Đặc t hình thc
Java Modeling Language
vJava Modeling Language (JML)
§http://www.eecs.ucf.edu/~leavens/JML/index.shtml
vTài liu:
§http://www.kindsoftware.com/products/opensource/ESCJava2/
docs.html
vNgôn ng đặc t hình thc cho Java
§đặc t hành vi ca các lp trong Java
§ghi li các quyết định v thiết kế và cài đặt
bng cách thêm vào trong mã ngun Java các assertion
§điu kin trước (pre-condition)
§điu kin sau (post-condition)
§bt biến (invariant)
vMc tiêu: người lp trình Java nào cũng có th
s dng d dàng.
3
Nguyn Th Minh Tuyn
Đặc t hình thc
vJML assertion được thêm vào dưới
dng các chú thích trong file .java
§/*@ ... @*/ hoc //@
vCác thuc tính được đặc t dưới dng
các biu thc boolean và được m
rng vi mt s toán t (\old, \forall,
\result, ...).
vs dng mt s t khóa ( requires,
ensures, signals, assignable, pure,
invariant, non_null, ...)
4
Nguyn Th Minh Tuyn
Đặc t hình thc
Điu kin trước và sau
(pre- và post-condition)
vĐiu kin trước ca mt phương thc
điu kin phi đúng trước khi gi
phương thc đó.
§S dng t khóa requires.
vĐiu kin sau ca mt phương thc là
điu kin phi đúng khi nó kết thúc.
§Điu kin sau bình thường đặc t cái gì phi đúng khi
phương thc tr v bình thường, nghĩa là không có
ngoi l. S dng t khóa ensures.
§Điu kin sau đặc t nhng gì xy ra khi có ngoi l.
S dng t khóa signals.
5
Nguyn Th Minh Tuyn