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
Các phép toán logic
v Những phép toán logic thường dùng
negation
! && conjunction disjunction || => implication alternative
not and or implies else
<=> iff
2 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Thứ tự ưu tiên các phép toán
thấp
cao
|| <=> => && ! = != in + - ++ & -> <: :> [ ] . ~ * ^
3 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Ví dụ
v Giả sử một sổ địa chỉ được mô hình hóa:
§ homeAddress và workAddress ánh xạ một bí danh (alias) tới địa
chỉ email cá nhân và dùng cho công việc, và địa chỉ ánh xạ một bí danh tới một địa chỉ thường dùng.
§ Để nói rằng địa chỉ thường dùng cho một bí danh a nào đó là địa chỉ email sử dụng cho công việc nếu nó tồn tại, nếu không đó sẽ là địa chỉ email cá nhân, ta có thể viết: some a.workAddress => a.address = a.workAddress else a.address = a.homeAddress hoặc sử dụng các biểu thức điều kiện a.address =
some a.workAddress => a.workAddress else a.homeAddress
4 Nguyễn Thị Minh Tuyền Đặc tả hình thức
v a!=b tương đương với not a = b có thể viết a not = b
v Từ khóa else có thể được dùng với toán tử implies
tương đương với (F and G) or (not F) and H
§ F implies G else H §
v Toán từ implies có thể lồng nhau
§ C1 implies F1 § else C2 implies F2 § else C3 implies F3 § với điều kiện C1 thì F1 đúng, nếu không với điều kiện C2 thì F2 đúng,
nếu không với điều kiện C3 thì F3 đúng.
v {F G H} tương đương F and G and H v C implies E1 else E2 có thể viết C => E1 else
E2.
5 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Ví dụ: Cấu trúc Family
v Làm sao để diễn đạt ràng buộc “Không ai có nhiều hơn một bố và và nhiều hơn một mẹ”? all p: Person | (lone (p.parents & Man)) and (lone (p.parents & Woman))
v Đây là một ví dụ về ràng buộc phủ định,
dễ hơn là phát biểu trực tiếp.
6 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Tập bằng cách định nghĩa thuộc tính
v { x : S | F } v Tập mà trong đó các giá trị được tạo ra từ
tập S thỏa mãn điều kiện F
v Sử dụng định nghĩa thuộc tính để đặc tả
tập những người có cùng bố mẹ với Matt { q: Person | q.parents = matt.parents }
7 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Ví dụ: cấu trúc Family
v Làm sao diễn đạt ràng buộc “Anh chị em của một người P là những người có cùng bố mẹ với P (ngoại trừ P)” all p: Person | p.siblings =
{q: Person | p.parents = q.parents} - p
8 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Ví dụ: Cấu trúc Family
v Mỗi người đàn ông/phụ nữ thì có một vợ/
chồng all p: Married |
(p in Man => p.spouse in Woman)
(p in Woman => p.spouse in Man)
and
v Một người vợ/chồng thì không thể là anh
chị em của nhau no p: Married |
p.spouse in p.siblings
9 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Let
v let x = e | A v Mỗi lần xuất hiện của biến x sẽ được thay
thế bởi biểu thức e trong A.
v Ví dụ: Mỗi người đàn ông/phụ nữ có gia
đình thì có một vợ/chồng all p: Married |
let spouse = p.spouse |
(p in Man => spouse in Woman) and (p in Woman => spouse in Man)
10 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Cardinality và số nguyên
v Các phép toán sau đây có thể được sử dụng
với số nguyên § plus § minus § mul § div § rem
cộng trừ nhân chia phần dư v và các phép toán so sánh bằng nhau bé hơn lớn hơn bé hơn hoặc bằng lớn hơn hoặc bằng
§ = § < § > § =< § >=
11 Nguyễn Thị Minh Tuyền Đặc tả hình thức
I’m my own GrandPa
12 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Mô hình Alloy đầu tiên khai báo module header
1 module language/grandpa1 2 abstract sig Person { 3 father: lone Man, 4 mother: lone Woman
Khai báo signature
5 } 6 sig Man extends Person {
7 wife: lone Woman 8 } 9 sig Woman extends Person {
Khai báo assertion
10 husband: lone Man 11 }
12 fact { 13 no p: Person | p in p.^(mother + father) 14 wife = ~husband 15 }
Ràng buộc
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
Lệnh
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
Fact
v Các ràng buộc trên signature và field được biểu diễn trong Alloy bằng cách sử dụng các fact.
v Các ràng buộc trong fact được giả sử
luôn luôn đúng. fact tên_fact{ --các ràng buộc }
v Thứ tự của các fact và thứ tự các ràng
buộc trong một fact không ảnh hưởng đến mô hình.
14 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Ví dụ: đèn giao thông
Junction
Light State
lights
Light
Color
Red
Yellow
Green
15 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Ví dụ: Đèn giao thông
all s: LightState, j: Junction | some s.color.Red & j.lights
Hệ thống đèn giao thông trong đó ở mỗi trạng thái, một số đèn tại giao lộ phải hiển thị màu đỏ. sig LightState {color: Light -> one Color} sig Light {} abstract sig Color {} one sig Red, Yellow, Green extends Color {} sig Junction {lights: set Light} fact { }
16 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Ví dụ
v Không ai có thể là tổ tiên của chính mình
fact selfAncestor {
no p: Person | p in p.^parents
}
v Có nhiều nhất một cha và nhiều nhất một mẹ
fact loneParents {
all p: Person | lone (p.parents & Man) and lone (p.parents & Woman)
}
v Anh chị em của một người P là những người có
cùng cha mẹ ngoại trừ P fact siblingsDefinition { all p: Person | p.siblings = {q: Person | p.parents = q.parents} – p
}
17 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Ví dụ
fact social { -- Mỗi người đàn ông/phụ nữ có gia đình thì có một vợ/chồng all p: Married | let s = p.spouse |
(p in Man => s in Woman) and (p in Woman => s in Man)
-- Một vợ/chồng không thể là anh em của nhau no p: Married | p.spouse in p.siblings -- Một người không thể cưới một người cùng huyết thống no p: Married |
some (p.*parents & (p.spouse).*parents)
}
18 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Hàm (function)
v Một hàm là một biểu thức được đặt
tên, với 0 hoặc nhiều tham số (argument), và một biểu thức giới hạn cho kết quả.
19 Nguyễn Thị Minh Tuyền Đặc tả hình thức
v Cú pháp: func tên [ ]{ } hoặc func tên [ danh sách các tham số ]{ }
Ví dụ
v Quan hệ parents
fun parents [ ] : Person->Person {~children}
v Quan hệ sisters (chị/em gái)
fun sisters [p: Person] {
{w: Woman | w in p.siblings}
}
v Không ai có thể là tổ tiên hay là chị/em
gái của chính họ all p: Person | not (p in p.^parents or
p in sisters[p])
20 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Vị từ (predicate)
v Một vị từ là một ràng buộc được đặt tên, với 0 hoặc nhiều tham số. Khi một vị từ được sử dụng, một biểu thức phải được cung cấp cho mỗi tham số.
v Cú pháp: pred tên [ ] { } hoặc pred tên [ danh sách các tham số ]{ }
21 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Ví dụ
v Hai người có cùng quan hệ huyết thống
nếu có cùng tổ tiên pred BloodRelated [p: Person, q: Person] {
some (p.*parents & q.*parents)
}
v Một người không thể cưới một người có
cùng huyết thống với mình no p: Married | BloodRelated[p, p.spouse]
22 Nguyễn Thị Minh Tuyền Đặc tả hình thức
Vị từ hay fact
v Vị từ là định nghĩa (được tham số
hóa) về các ràng buộc.
v Fact là các ràng buộc được giả sử là
đúng.
v Có thể đặt các ràng buộc trong các vị từ và đặt các vị từ đó vào các fact. § Vị từ linh động hơn fact.
23 Nguyễn Thị Minh Tuyền Đặc tả hình thức
