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

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