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

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