LOGO
Đặc tả hình thức
Nguyễn Thị Minh Tuyền
Các module trong Alloy
Nguyễn Thị Minh Tuyền 1
Đặc tả hình thức
Module trong Alloy
v Alloy là một hệ thống module cho
phép module hóa việc sử dụng lại các
mô hình.
v Một module định nghĩa một mô hình
và có thể xem mô hình này là một mô
hình con của mô hình khác.
v Để thuận lợi cho việc tái sử dụng, các
module có thể được tham số hóa
trong một hoặc nhiều signature
2
Nguyễn Thị Minh Tuyền
Đặc tả hình thức
Ví dụ
module util/relation
-- r is acyclic over the set s
pred acyclic [r: univ->univ, s: set univ] {
all x: s | x !in x.^r
}
module family
open util/relation as rel
sig Person {
parents: set Person
}
fact { acyclic [parents, Person] }
3
Nguyễn Thị Minh Tuyền
Đặc tả hình thức
Ví dụ
module util/relation
-- r is acyclic over the set s
pred acyclic [r: univ->univ, s: set univ] {
all x: s | x !in x.^r
}
module fileSystem
open util/relation as rel
sig Object {}
sig Folder extends Object {
subFolders: set Folder
}
fact { acyclic [subFolders, Folder] }
4
Nguyễn Thị Minh Tuyền
Đặc tả hình thức
Khai báo module
v Dòng đầu tiên của mỗi module là
module header
module modulePathName
v Module có thể import một module
khác với câu lệnh open ngay sau
header
open modulePathName
5
Nguyễn Thị Minh Tuyền