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

LOGO<br /> <br /> Đặc tả hình thức<br /> Mô hình động trong Alloy<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 1<br /> <br /> Các mô hình tĩnh<br /> v Trong các buổi học trước<br /> §  định nghĩa các mô hình dựa vào tập hợp và quan hệ<br /> <br /> v Một instance của mô hình là một tập các<br /> giá trị thỏa mãn các ràng buộc được định<br /> nghĩa bởi multiplicity, fact,..<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 2<br /> <br /> Đặc tả hình thức<br /> <br /> Các mô hình tĩnh<br /> Person = {Matt, Sue}<br /> Man = {Matt}<br /> Woman = {Sue}<br /> Married = {}<br /> spouse = {}<br /> children = {}<br /> siblings = {}<br /> <br /> Person = {Matt, Sue}<br /> Man = {Matt}<br /> Woman = {Sue}<br /> Married = {Matt, Sue}<br /> spouse = {(Matt,Sue), (Sue,Matt)}<br /> children = {}<br /> siblings = {}<br /> <br /> Person = {Matt, Sue, Sean}<br /> Man = {Matt}<br /> Woman = {Sue}<br /> Married = {Matt, Sue}<br /> spouse = {(Matt,Sue), (Sue,Matt)}<br /> children = {(Matt,Sean), (Sue,Sean)}<br /> siblings = {}<br /> Nguyễn Thị Minh Tuyền<br /> <br /> 3<br /> <br /> Đặc tả hình thức<br /> <br /> Mô hình động<br /> v Các mô hình tĩnh cho phép mô tả trạng<br /> thái hợp lệ của một hệ thống động.<br /> v Ta cũng có thể mô tả các chuyển đổi hợp<br /> lệ giữa các trạng thái.<br /> v Ví dụ:<br /> §  Một người được sinh ra trước khi họ cưới<br /> §  Một người kết hôn trước khi có con<br /> §  Một người là con cho đến khi họ chết<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 4<br /> <br /> Đặc tả hình thức<br /> <br /> Ví dụ<br /> abstract sig Person {<br /> children: set Person,<br /> siblings: set Person<br /> }<br /> sig Man, Woman extends Person {}<br /> sig Married in Person {<br /> spouse: one Married<br /> }<br /> <br /> Nguyễn Thị Minh Tuyền<br /> <br /> 5<br /> <br /> Đặc tả hình thức<br /> <br />