Đang chuẩn bị liên kết để tải về tài liệu:
Bài giảng Đặc tả hình thức: Chương 12 - Nguyễn Thị Minh Tuyền

Nội dung chương 12 trình bày đến người học những vấn đề liên quan đến "Giới thiệu về ESC/Java2 Thủ thuật và cạm bẫy", cụ thể như: Đặc tả thừa kế, Aliasing, Object invariants, giả thuyết không nhất quán, Exposed references, old, viết đặc tả thế nào,. | LOGO Đặc tả hình thức Giới thiệu về ESC/Java2 Thủ thuật và cạm bẫy Nguyễn Thị Minh Tuyền Nội dung slide này được dịch từ các slide của David Cok, Joe Kiniry, Eric Poll 1 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 Nguyễn Thị Minh Tuyền 2 Đặ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 Nguyễn Thị Minh Tuyền 3 Đặ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. Nguyễn Thị Minh Tuyền 4 Đặ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ó. Nguyễn Thị Minh Tuyền 5 Đặc tả hình .