tailieunhanh - 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. ! | 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 & } 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 | = } 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 & ) } 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 .