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

LOGO<br /> <br /> Đặc tả hình thức<br /> JML nâng cao<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 /> Từ khóa chính trong JML<br /> v requires<br /> v ensures<br /> v signals<br /> v assignable<br /> v normal_behavior<br /> v invariant<br /> v non_null<br /> v pure<br /> v \old, \forall, \exists, \result<br /> Nguyễn Thị Minh Tuyền<br /> <br /> 2<br /> <br /> Đặc tả hình thức<br /> <br /> Các tính năng nâng cao<br /> v Visibility<br /> v Đặc tả các ngoại lệ<br /> v Mệnh đề assignable và nhóm dữ liệu<br /> v Aliasing<br /> v Thừa kế đặc tả, ensuring behavioural<br /> subtyping<br /> v Các trường chỉ ở mức đặc tả: ghost và<br /> model<br /> v Ngữ nghĩa của invariant<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 3<br /> <br /> Đặc tả hình thức<br /> <br /> v Visibility<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 4<br /> <br /> Đặc tả hình thức<br /> <br /> Visibility<br /> v JML áp dụng các quy tắt về visibility<br /> tương tự như Java.<br /> v Ví dụ:<br /> public class Bag{ <br /> ... <br /> private int n; <br /> //@ requires n > 0; <br /> public int extractMin(){ ... } <br /> <br /> không phải là kiểu hợp lệ, vì visibility<br /> của phương thức extractMin là public<br /> chỉ đến trường n có visibility là private.<br /> Nguyễn Thị Minh Tuyền<br /> <br /> 5<br /> <br /> Đặc tả hình thức<br /> <br />