Xem mẫu
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
not
!
and
&&
or
||
implies
=>
else
Nguyễn Thị Minh Tuyền
logic thường dùng
negation
conjunction
disjunction
implication
alternative
iff
2
Đặc tả hình thức
Thứ tự ưu tiên các phép toán
||
=>
&&
!
= != in
+ ++
&
->
[]
.
~ * ^
Nguyễn Thị Minh Tuyền
thấp
cao
3
Đặ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
Nguyễn Thị Minh Tuyền
4
Đặ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.
Nguyễn Thị Minh Tuyền
5
Đặc tả hình thức
nguon tai.lieu . vn
Đặ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
not
!
and
&&
or
||
implies
=>
else
Nguyễn Thị Minh Tuyền
logic thường dùng
negation
conjunction
disjunction
implication
alternative
iff
2
Đặc tả hình thức
Thứ tự ưu tiên các phép toán
||
=>
&&
!
= != in
+ ++
&
->
[]
.
~ * ^
Nguyễn Thị Minh Tuyền
thấp
cao
3
Đặ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
Nguyễn Thị Minh Tuyền
4
Đặ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.
Nguyễn Thị Minh Tuyền
5
Đặc tả hình thức