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