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

Assertion là ràng buộc bổ sung và được kiểm tra bởi bộ phân tích xem chúng có đúng hay không. Bài giảng Đặc tả hình thức: Chương 5 do Nguyễn Thị Minh Tuyền sau đây sẽ giúp các bạn nắm chi tiết hơn về Assertion. Mời các bạn cùng tham khảo!
Nội dung trích xuất từ tài liệu:
Bài giảng Đặc tả hình thức: Chương 5 - Nguyễn Thị Minh Tuyền LOGO Đặc tả hình thức Giới thiệu về Alloy Nguyễn Thị Minh Tuyền Nguyễn Thị Minh Tuyền 1 Assertion v Assertion là ràng buộc bổ sung và được kiểm tra bởi bộ phân tích xem chúng có đúng hay không. v Nếu một assertion không đúng, bộ phân tích sẽ tạo ra một phản ví dụ. v Cú pháp: assert tên{ --ràng buộc } Nguyễn Thị Minh Tuyền 2 Đặc tả hình thức Ví dụ v Không ai có bố mẹ mà đồng thời cũng là anh chị em. assert parentsSiblings{ all p: Person | no p.parents & p.siblings } v Anh chị em của một người là anh chị em của những người đó. assert siblingsSiblings{ all p: Person | p.siblings = p.siblings.siblings } v Không ai có cùng tổ tiên với chồng/vợ mình ( ví dụ vợ/chồng không có quan hệ huyết thống). assert sameBlood{ no p: Married | some (p.^parents & p.spouse.^parents) } Nguyễn Thị Minh Tuyền 3 Đặc tả hình thức Lệnh (command) và phạm vi (scope) v Để phân tích một mô hình, ta cần một lệnh và chỉ dẫn công cụ thực thi nó. §  Lệnh run yêu cầu công cụ tìm kiếm một instance của một vị từ. §  Lệnh check yêu cầu công cụ tìm kiếm một phản ví dụ của một assertion. §  Ví dụ: •  check Safe •  run trans v Để chỉ rõ một phạm vi, ta có thể đưa ra một giới hạn (scope )cho mỗi signature tương ứng với một loại cơ bản. Nguyễn Thị Minh Tuyền 4 Đặc tả hình thức Check v assert a {F} v check a scope Nếu mô hình có các fact M, tìm một ví dụ sao cho M && !F v check a for default v check a for default but list v check a for list Nguyễn Thị Minh Tuyền 5 Đặc tả hình thức