LOGO
Đặc tả hình thức
Giới thiệu về Alloy
Nguyễn Thị Minh Tuyền
Nguyễn Thị Minh Tuyền 1
Assertion
v Assertion là ràng buộc bổ sung và được kiểm tra bởi bộ phân tích xem chúng có đúng hay không.
v Nếu một assertion không đúng, bộ phân tích
sẽ tạo ra một phản ví dụ.
v Cú pháp: assert tên{
--ràng buộc
}
2 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Ví dụ
v Không ai có bố mẹ mà đồng thời cũng là anh chị
em. assert parentsSiblings{
all p: Person | no p.parents & p.siblings
}
v Anh chị em của một người là anh chị em của
những người đó. assert siblingsSiblings{
all p: Person | p.siblings = p.siblings.siblings
}
v Không ai có cùng tổ tiên với chồng/vợ mình ( ví dụ vợ/chồng không có quan hệ huyết thống). assert sameBlood{
no p: Married | some (p.^parents & p.spouse.^parents)
}
3 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Lệnh (command) và phạm vi (scope)
v Để phân tích một mô hình, ta cần một lệnh
và chỉ dẫn công cụ thực thi nó. § Lệnh run yêu cầu công cụ tìm kiếm một instance của một vị từ. § Lệnh check yêu cầu công cụ tìm kiếm một phản ví dụ của một
assertion.
§ Ví dụ:
• check Safe • run trans
v Để chỉ rõ một phạm vi, ta có thể đưa ra một giới hạn (scope )cho mỗi signature tương ứng với một loại cơ bản.
4 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Check
v assert a {F} v check a scope Nếu mô hình có các fact M, tìm một ví dụ sao cho M && !F v check a for default v check a for default but list v check a for list
5 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Ví dụ về check
v Ví dụ: Cho trước các khai báo của một
hệ thống file: abstract sig Object {} sig Directory extends Object {} sig File extends Object {} sig Alias extends File {}
v và một assertion A. Các lệnh sau đây
là đúng cú pháp § check A for 5 Object § check A for 4 Directory, 3 File § check A for 5 Object, 3 Directory § check A for 3 Directory, 3 Alias, 5 File
6 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Ví dụ về check
v Ta có thể thiết lập một phạm vi mặc định, và có thể trộn lẫn giữa phạm vi mặc định với giới hạn rõ ràng cho một loại cụ thể.
v Ví dụ:
§ check A for 5 § Đặt một giới hạn là 5 cho tất cả các loại top-level. § check A for 5 but 3 Directory § đặt thêm một giới hạn là 3 cho Directory, và một giới hạn là 2
cho File bằng phép suy dẫn.
v Có thể dùng từ khóa exactly:
§ check A for exactly 3 Directory, exactly 3 Alias, 5 File § Giới hạn File với nhiều nhất 5 phần tử, nhưng yêu cầu Directory
và Alias có chính xác 3 phần tử cho mỗi loại.
7
Nguyễn Thị Minh Tuyền
Đặc tả hình thức
Câu hỏi
v Nếu AA không tìm được một phản ví
dụ cho assertion thì assertion có hợp lệ không?
8 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Run
v Được dùng để yêu cầu AA sinh ra các
instance của mô hình.
v AA chỉ thực thi lệnh run đầu tiên
trong file.
v Để phân tích một mô hình, thêm lệnh
run và chỉ dẫn AA thực thi nó.
v Có thể cung cấp cho lệnh run một
phạm vi § giới hạn kích thước các instance được xem xét.
9 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Run và vị từ
v pred p[x:X, y:Y,...] {F} v run p scope v Nếu mô hình có các fact M, tìm ví dụ
sao cho M && (some x:X, y:Y|F)
v fun f[x:X,y:Y,...] R{E} v run f scope v Nếu mô hình có các fact M, tìm ví dụ
sao cho
v M && (some x:X, y:Y,...,result:R|result =
E)
10 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Ví dụ về lệnh run
v Lệnh run đơn giản nhất
§ run {}
v Lệnh run có điều kiện
§ run {some Man && some Woman && some Married}
for 2
v Một số kịch bản khác
§ run {some Woman && no Man} for 7 § run {some Man && some Married && no Woman}
11 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Câu hỏi
v sử dụng lệnh run cho một vị từ và
check cho một assertion có khác nhau không?
12 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Trở lại ví dụ granpa
1 module language/grandpa1 2 abstract sig Person { 3 father: lone Man, 4 mother: lone Woman
5 } 6 sig Man extends Person {
7 wife: lone Woman 8 } 9 sig Woman extends Person {
10 husband: lone Man 11 }
12 fact { 13 no p: Person | p in p.^(mother + father) 14 wife = ~husband 15 }
16 assert NoSelfFather { 17 no m: Man | m = m.father
18 } 19 check NoSelfFather
20 fun grandpas (p: Person): set Person { 21 p.(mother + father).father
22 } 23 pred ownGrandpa (p: Person) { 24 p in grandpas [p]
25 } 26 run ownGrandpa for 4
13 Nguyễn Thị Minh Tuyền Đặc tả hình thức
