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

hép toán tập hợp §  + hợp §  & giao §  - hiệu §  in tập con §  = bằng nhau v nghĩa là §  một tuple trong p+q khi nó ở trong p hoặc trong q §  một tuple ở trong p & q khi nó ở trong p và ở trong q §  một tuple ở trong p-q khi nó ở trong p nhưng không ở trong q §  p in q đúng khi mọi tuple của p cũng là một tuple của q §  p=q đúng khi p và q có cùng các tuple 50 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ v Cho các tập sau: §  Name = {(G0), (A0), (A1)} §  Alias = {(A0), (A1)} §  Group = {(G0)} §  RecentlyUsed = {(G0), (A1)} v Alias + Group = {(G0), (A0), (A1)} §  cho một tập các nguyên tử là Alias hoặc Group; v Alias & RecentlyUsed = {(A1)} §  cho một tập các nguyên tử là alias và vừa đươc sử dụng gần đây v Name - RecentlyUsed = {(A0)} §  cho tập các nguyên tử là các tên không được sử dụng gần đây 51 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ v RecentlyUsed in Alias §  mọi thứ được sử dụng gần đây là alias, và điều này sai vì tuple {(G0)} không được sử dụng nhưng một alias v Name = Group + Alias §  mọi tên là một nhóm hoặc một alias và ngược lại, mọi nhóm hoặc alias là tên, điều này là đúng. 52 Nguyễn Thị Minh Tuyền Đặc tả hình thức Phép toán quan hệ §  -> arrow (product) §  ~ chuyển vị §  . dot join §  [] box join §  ^ transitive closure §  * reflexive-transitive closure §  <: giới hạn miền (domain restriction) §  :> giới hạn ảnh (image restriction) §  ++ override 53 Nguyễn Thị Minh Tuyền Đặc tả hình thức Arrow Product v  p -> q v  p và q là hai quan hệ v  p->q là quan hệ có được bằng cách lấy mỗi kết hợp của một tuple từ p và một tuple từ q và nối chúng với nhau v  Khi p và q là các tập hợp, p->q là quan hệ nhị phân v  Khi p và q là các tuple, p->q cũng là một tuple. v  Ví dụ: Name = {(N0),(N1)} Addr = {(D0),(D1)} Book = {(B0)} Name -> Addr = {(N0,D0),(N0,D1),(N1,D0),(N1,D1)} là quan hệ ánh xạ tất cả các tên thành tất cả các địa chỉ Book -> Name -> Addr = {(B0,N0,D0),(B0,N0,D1),(B0,N1,D0),(B0,N1,D1)} là quan hệ liên quan đến sách, tên và địa chỉ ở tất cả các trường hợp có thể có. 54 Nguyễn Thị Minh Tuyền Đặc tả hình thức Chuyển vị v ~ p v lấy ảnh đối xứng của quan hệ p, nghĩa là đảo ngược thứ tự các phần tử trong mỗi tuple. v Ví dụ: §  example = {(a0,a1,a2,a3), (b0,b1,b2,b3)} §  ~example = {(a3,a2,a1,a0), (b3,b2,b1,b0)} v Biểu diễn mối quan hệ cha mẹ sử dụng ~ như thế nào? §  ~children 55 Nguyễn Thị Minh Tuyền Đặc tả hình thức Dot join hai tuple v p.q : Thực hiện dot join hai tuple này lại với nhau thì kết quả là gì? (s1,...,sm) (t1,...,tm) v Nếu sm ≠ t1 thì kết quả là rỗng v Nếu sm = t1 thì kết quả sẽ là: (s1,...,sm-1,t2,...,tm) v Ví dụ: §  {(a,b)}.{(a,c)} = {} §  {(a,b)}.{(b,c)} = {(a,c)} v Vậy {(a)} . {(a)} ? Không được định nghĩa v p.s được định nghĩa nếu và chỉ nếu p và s không phải là quan hệ đơn. 56 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ v {(N0, A0)} . {(A0, D0)} = {(N0, D0)} v {(N0, D0)} . {(N0, D0)} = {} v {(N0, D0)} . {(D1)} = {} v {(N0)} . {(N0, D0)} = {(D0)} v {(N0, D0)} . {(D0)} = {(N0)} v {(B0)} . {(B0, N0, D0)} = {(N0, D0)} 57 Nguyễn Thị Minh Tuyền Đặc tả hình thức Bài tập v Kết quả của phép toán sau là gì? {(a,b)}.{(c)} {(a)}.{(a,b)} {(a,b)}.{(b)} {(a)}.{(a,b,c)} {(a,b,c)}.{(c)} {(a,b)}.{(a,b,c)} {(a,b,c,d)}.{(d,e,f)} {(a)}.{(b)} 58 Nguyễn Thị Minh Tuyền Đặc tả hình thức Dot join hai quan hệ v p.q v p và q là hai quan hệ mà trong đó các quan hệ này không được đồng thời là hai quan hệ đơn. v p.q là quan hệ có được bằng cách lấy mỗi kết hợp của một tuple từ p và một tuple từ q và nối lại với nhau nếu có thể. 59 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ v to: ánh xạ một message thành tên mà nó định gởi đến. v address: ánh xạ tên thành địa chỉ. §  to = {(M0,N0),(M0,N2), (M1,N2),(M2,N3)} §  address = {(N0,D0), (N0,D1),(N1,D1),(N2,D3)} v to.address ánh xạ message thành địa chỉ mà nó định gởi §  to.address = {(M0,D0), (M0,D1),(M0,D3),(M1,D3)} 60 Nguyễn Thị Minh Tuyền M0 M1 M2 N0 N1 N2 N3 D0 D1 D3 to address Đặc tả hình thức Ví dụ v Sử dụng phép join để tìm ra các con của Matt và cháu của Matt §  matt.children // Matt’s children §  matt.children.children // Matt’s grandchildren 61 Nguyễn Thị Minh Tuyền Đặc tả hình thức Box Join v p[q] v Về mặt ngữ nghĩa thì giống như dot join, nhưng nó lấy các tham số ở thứ tự khác §  p[q] ≡ q.p v Ví dụ: con hoặc cháu của Matt? §  children[matt] // Matt’s children §  children.children[matt] // Matt’s grandchildren §  children[children[matt]] // Matt’s grandchildren 62 Nguyễn Thị Minh Tuyền Đặc tả hình thức Transitive Closure v Một quan hệ nhị phân là transitive nếu khi trong các tuple a->b và b->c thì nó cũng chứa a->c, hay nói cách khác r.r in r v Transitive closure ^r của một quan hệ nhị phân r: S x S là những gì có được sau khi điều hướng thông qua r cho đến khi không đi xa hơn được nữa. ^r = r + r.r + r.r.r+... 63 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ v  Một quan hệ address biểu diễn một danh sách địa chỉ với nhiều mức (ánh xạ các alias và group đến các group, alias và địa chỉ) và transitive closure của nó là: 64 Nguyễn Thị Minh Tuyền G0 A0 D0 G1 A1 D1 A2 D2 address = {(G0,A0),(G0,G1),(A0,D0),(G1,D0),(G1,A1),(A1,D1),(A2,D2)} ^address = {(G0,A0),(G0,G1),(A0,D0),(G1,D0),(G1,A1),(A1,D1),(A2,D2), (G0,D0),(G0,A1),(G1,D1),(G0,D1)} address ^address - address Đặc tả hình thức Ví dụ v Nếu ta muốn tìm tổ tiên hay con cháu của Matt thì làm thế nào? §  matt.^children // Matt’s descendants §  matt.^(~children) // Matt’s ancestors v Để biểu diễn “Không có người nào là tổ tiên của chính họ” thì làm thế nào? §  no p: Person | p in p.^(~children) 65 Nguyễn Thị Minh Tuyền Đặc tả hình thức Reflexive-transitive closure v Một quan hệ là reflexive nếu nó chưa tuple a-> cho mỗi nguyên tử a. Hay nói cách khác iden in r. v Một reflexive-transitive closure *r được định nghĩa bởi *r = ^r + iden v Ví dụ: 66 Nguyễn Thị Minh Tuyền (S0,S1) (S1,S2) (S2,S3) (S4,S7) (S0,S1) (S1,S2) (S2,S3) (S4,S7) (S0,S2) (S0,S3) (S1,S3) (S0,S0) (S1,S1) (S2,S2) (S3,S3) (S4,S4) (S7,S7) r *r ^r Đặc tả hình thức Giới hạn miền và ảnh v Phép toán giới hạn được sử dụng để lọc các quan hệ từ một miền hay ảnh cho trước. v Nếu s là một tập hợp và r là một quan hệ thì v s <: r chứa các tuple của r bắt đầu với một phần tử trong s v r :> s chứa các tuple của r kết thúc với một phần tử trong s v Ví dụ: §  Man = {(M0),(M1),(M2),(M3)} §  Woman = {(W0),(W1)} §  children = {(M0,M1),(M0,M2),(M3,W0),(W1,M1)} §  Man <: children = {(M0,M1),(M0,M2),(M3,W0)}// father-child §  children :> Man = {(M0,M1),(M0,M2),(W1,M1)}// parent-son 67 Nguyễn Thị Minh Tuyền Đặc tả hình thức Override v p ++ q v p và q là hai quan hệ với bậc bằng 2 hoặc hơn v Kết quả giống như hợp giữa p và q ngoại trừ các tuple của q có thể thay thế các tuple của p. v Bất cứ tuple nào trong p khớp với một tuple trong q bắt đầu với cùng phần tử thì loại bỏ. §  p ++ q = p – (domain(q) <: p) + q v Ví dụ: §  oldAddr = {(N0,D0),(N1,D1),(N1,D2)} §  newAddr = {(N1,D4),(N3,D3)} §  oldAddr ++ newAddr = {(N0,D0),(N1,D4),(N3,D3)} 68 Nguyễn Thị Minh Tuyền LOGO