LOGO
Đặc tả hình thức
Nguyễn Thị Minh Tuyền
Giới thiệu về Alloy
Nguyễn Thị Minh Tuyền 1
Đặc tả hình thức
Các phép toán logic
v Những phép toán logic thường dùng
not ! negation
and && conjunction
or || disjunction
implies => implication
else alternative
<=> 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
||
<=>
=>
&&
!
= != in
+ -
++
&
->
<:
:>
[ ]
.
~ * ^
3
Nguyễn Thị Minh Tuyền
thấp
cao
Đặ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
§ F implies G else H
§ tương đương với (F and G) or (not F) and 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