Bài giảng Đặc tả hình thức - Chương 4: Giới thiệu về Alloy - Nguyễn Thị Minh Tuyền (Tiếp)

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 Đặ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) 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 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 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 §  < 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 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 khai báo module header Khai báo signature Ràng buộc Khai báo assertion Lệnh Đặ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 15 Nguyễn Thị Minh Tuyền Junction Light Color Red Yellow Green lights Light State Đặc tả hình thức 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 } 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ả. v Cú pháp: func tên [ ]{ } hoặc func tên [ danh sách các tham số ]{ } 19 Nguyễn Thị Minh Tuyền Đặc tả hình thức 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 LOGO