Xem mẫu
LOGO
Đặc tả hình thức
Mô hình động trong Alloy
Nguyễn Thị Minh Tuyền
Nguyễn Thị Minh Tuyền
1
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,..
Nguyễn Thị Minh Tuyền
2
Đặc tả hình thức
Các mô hình tĩnh
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 = {}
Nguyễn Thị Minh Tuyền
3
Đặ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
Nguyễn Thị Minh Tuyền
4
Đặ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
}
Nguyễn Thị Minh Tuyền
5
Đặc tả hình thức
nguon tai.lieu . vn
Đặc tả hình thức
Mô hình động trong Alloy
Nguyễn Thị Minh Tuyền
Nguyễn Thị Minh Tuyền
1
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,..
Nguyễn Thị Minh Tuyền
2
Đặc tả hình thức
Các mô hình tĩnh
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 = {}
Nguyễn Thị Minh Tuyền
3
Đặ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
Nguyễn Thị Minh Tuyền
4
Đặ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
}
Nguyễn Thị Minh Tuyền
5
Đặc tả hình thức