Giáo trình Đặc tả hình thức - Chương 4: Giới thiệu về Alloy - Nguyễn Thị Minh Tuyền

Nội dung text: Giáo trình Đặc tả hình thức - Chương 4: Giới thiệu về Alloy - Nguyễn Thị Minh Tuyền

1. 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
2. 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 Nguyễn Thị Minh Tuyền 2 Đặc tả hình thức
3. Thứ tự ưu tiên các phép toán || thấp => && ! = != in + - ++ & -> [ ] cao . ~ * ^ Nguyễn Thị Minh Tuyền 3 Đặc tả hình thức
4. 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
5. 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
6. 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. Nguyễn Thị Minh Tuyền 6 Đặc tả hình thức
7. 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 } Nguyễn Thị Minh Tuyền 7 Đặc tả hình thức
8. 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 Nguyễn Thị Minh Tuyền 8 Đặc tả hình thức
9. 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) and (p in Woman => p.spouse in Man) 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 Nguyễn Thị Minh Tuyền 9 Đặc tả hình thức
10. 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) Nguyễn Thị Minh Tuyền 10 Đặc tả hình thức
11. 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 cộng § minus trừ § mul nhân § div chia § rem phần dư v và các phép toán so sánh § = bằng nhau § lớn hơn § = = lớn hơn hoặc bằng Nguyễn Thị Minh Tuyền 11 Đặc tả hình thức
12. I’m my own GrandPa Nguyễn Thị Minh Tuyền 12 Đặc tả hình thức
13. Mô hình Alloy đầu tiên 1 module language/grandpa1 khai báo 2 abstract sig Person { module header 3 father: lone Man, 4 mother: lone Woman 5 } 6 sig Man extends Person { Khai báo 7 wife: lone Woman 8 } signature 9 sig Woman extends Person { 10 husband: lone Man 11 } 12 fact { Khai báo 13 no p: Person | p in p.^(mother + father) 14 wife = ~husband assertion 15 } 16 assert NoSelfFather { 17 no m: Man | m = m.father 18 } 19 check NoSelfFather Ràng buộc 20 fun grandpas (p: Person): set Person { 21 p.(mother + father).father 22 } 23 pred ownGrandpa (p: Person) { 24 p in grandpas [p] Lệnh 25 } 26 run ownGrandpa for 4 Nguyễn Thị Minh Tuyền 13 Đặc tả hình thức
14. 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. Nguyễn Thị Minh Tuyền 14 Đặc tả hình thức
15. Ví dụ: đèn giao thông Light Junction State lights Light Color Red Yellow Green Nguyễn Thị Minh Tuyền 15 Đặc tả hình thức
16. Ví dụ: Đèn giao thông 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 { all s: LightState, j: Junction | some s.color.Red & j.lights } Nguyễn Thị Minh Tuyền 16 Đặc tả hình thức
17. 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 } Nguyễn Thị Minh Tuyền 17 Đặc tả hình thức
18. 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) } Nguyễn Thị Minh Tuyền 18 Đặc tả hình thức
19. 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ả. v Cú pháp: func tên [ ]{ } hoặc func tên [ danh sách các tham số ]{ } Nguyễn Thị Minh Tuyền 19 Đặc tả hình thức
20. 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]) Nguyễn Thị Minh Tuyền 20 Đặc tả hình thức
21. 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ố ]{ } Nguyễn Thị Minh Tuyền 21 Đặc tả hình thức
22. 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] Nguyễn Thị Minh Tuyền 22 Đặc tả hình thức
23. 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. Nguyễn Thị Minh Tuyền 23 Đặc tả hình thức