LOGO
Đặc tả hình thức
Nguyễn Thị Minh Tuyền
1
Giới thiệu về ESC/Java2
Thủ thuật và cạm bẫy
Nội dung slide này được dịch từ các slide của David Cok, Joe Kiniry, Eric Poll
Đặc tả hình thức
Nội dung
1. Đặc tả thừa kế
2. Aliasing
3. Object invariants
4. Giả thuyết không nhất quán
5. Exposed references
6. \old
7. Viết đặc tả thế nào
2
Nguyễn Thị Minh Tuyền
Đặc tả hình thức
Nội dung
1. Đặc tả thừa kế
2. Aliasing
3. Object invariants
4. Giả thuyết không nhất quán
5. Exposed references
6. \old
7. Viết đặc tả thế nào
3
Nguyễn Thị Minh Tuyền
Đặc tả hình thức
Behavioural subtyping
v Giả sử rằng Child mở rộng từ Parent
§ Behavioural subtyping = các đối tượng từ lớp con
Child ứng xử giống các đối tượng từ lớp cha Parent.
§ Nguyên tắc: mã nguồn sẽ ứng xử như mong đợi nếu
ta khai báo một đối tượng Child trong đó một đối
tượng Parent đã được cài đặt như mong đợi.
4
Nguyễn Thị Minh Tuyền
Đặc tả hình thức
Behavioural subtyping
v Một số ràng buộc bởi behavioural
subtyping:
§ Bất biến trong lớp con mạnh hơn bất biến trong lớp
cha.
§ Đối với mỗi phương thức:
• Điều kiện trước trong lớp con yếu hơn điều kiện trước
trong lớp cha
• Điều kiện sau trong lớp con mạnh hơn điều kiện sau
trong lớp cha.
v JML đạt được behavioural subtyping
bằng kế thừa đặc tả: bất cứ lớp con
nào cũng kế thừa đặc tả từ lớp cha
của nó.
5
Nguyễn Thị Minh Tuyền