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

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