Đặc tả hình thức - Giới thiệu về Alloy - Nguyễn Thị Minh Tuyền

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 Nội dung v Nguyên tử và quan hệ v Signature và Field v Các phép toán 2 Nguyễn Thị Minh Tuyền Đặc tả hình thức Tài liệu tham khảo v Sách tham khảo: §  Software Abstractions: Logic, Language, and Analysis, Revised edition, Daniel Jackson, 2012 v Tải phần mềm + tài liệu + ví dụ mẫu: §  3 Nguyễn Thị Minh Tuyền Đặc tả hình thức v Alloy chỉ là một trong các phương pháp phân tích và mô hình hóa theo hướng trừu tượng hóa phần mềm. §  B, OCL (Object Constraint Language), VDM (Vienna Development Method), Z. v Điểm chung: §  Cung cấp những khái niệm về trừu tượng hóa phần mềm một cách ngắn gọn và trực tiếp hơn so với các ngôn ngữ lập trình. §  Dựa vào cấu trúc toán học cổ điển: tập hợp và quan hệ §  Mô tả hành vi (behavior) theo kiểu khai báo. §  Sử dụng các ràng buộc. 4 Nguyễn Thị Minh Tuyền Đặc tả hình thức Một số điểm khác nhau v B §  Khái niệm của nó hơi giống ngôn ngữ lập trình trừu tượng hơn là ngôn ngữ đặc tả. v OCL §  Rất khác về mặt cú pháp v B, VDM và Z được thiết kế thiên về chứng minh (proof) hơn là phân tích đơn giản. v B, VDM và Z diễn đạt tốt hơn Alloy §  Cấu trúc của Alloy chỉ hỗ trợ logic bậc nhất (first order logic) §  Các ngôn ngữ khác hỗ trợ cả cấu trúc bậc cao và cả quantification nữa. v Alloy hỗ trợ kém về số nguyên và chuỗi 5 Nguyễn Thị Minh Tuyền Đặc tả hình thức Alloy và UML v Khái niệm đồ họa, các ràng buộc OCL tương tự UML nhưng Alloy gọn nhẹ và chính xác hơn. v UML có nhiều khái niệm mô hình hóa mà Alloy bỏ qua (biểu đồ use case, biểu đồ trạng thái, ) v Biểu đồ và quan hệ trong Alloy dựa vào UML. 6 Nguyễn Thị Minh Tuyền Đặc tả hình thức Alloy – Đặc điểm v Nhỏ gọn, dễ sử dụng, có khả năng biểu diễn các thuộc tính một cách ngắn gọn và tự nhiên. v Ngữ nghĩa về toán học đơn giản và đồng nhất. v Phân tích ngữ nghĩa tự động một cách hoàn chỉnh và hiệu quả. 7 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ v Ta muốn biểu diễn §  Mô hình hóa mối quan hệ bố mẹ/con cái §  Mô hình hóa quan hệ vợ chồng §  Mô hình hóa quan hệ anh chị em. §  Tăng cường một số ràng buộc sinh học thông qua vị từ thứ tự bậc nhất (ví dụ chỉ có 1 mẹ) §  Tăng cường một số ràng buộc xã hội thông qua vị từ bậc nhất (ví dụ vợ không phải là anh em) §  Xác nhận hoặc biện luận sự tồn tại của một số quan hệ (ví dụ không ai có vợ mà người đó cùng bố mẹ với mình) 8 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ 2 v Một danh sách email của khách hàng. Từ tên khách hàng ta có thể lấy được địa chỉ email. 9 Nguyễn Thị Minh Tuyền FriendBook Ted -> ted@gmail.com Ryan -> ryan@hotmail.com WorkBook Pilard -> pilard@hcmus.edu.vn Ryan -> ryan@hcmus.edu.vn Đặc tả hình thức Nội dung v Nguyên tử và quan hệ v Signature và Field v Các phép toán 10 Nguyễn Thị Minh Tuyền Đặc tả hình thức Nguyên tử (atom) và quan hệ v Trong Alloy, mọi thứ được xây dựng từ các nguyên tử và quan hệ. v Một nguyên tử là một thực thể sơ khai §  Indivisible: nó không thể chia thành những phần nhỏ hơn. §  Immutable: thuộc tính của nó không thay đổi theo thời gian. §  Uninterpreted: nó không được thiết lập thuộc tính (các con số chẳng hạn). v Một quan hệ là một cấu trúc liên quan đến các nguyên tử. Đó là một tập hợp các tuple, mỗi tuple là một chuỗi tuần tự các nguyên tử. 11 Nguyễn Thị Minh Tuyền Đặc tả hình thức Nguyên tử và quan hệ v Một quan hệ đơn phân tương đương với một bảng có một cột. §  Nó biểu diễn một tập các nguyên tử. v Một quan hệ đơn phân với chỉ có một tuple, tương đương với một bảng và một đầu vào đơn, biểu diễn một scalar. 12 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ v Quan hệ đơn phân: một tập các tên, tập các địa chỉ và tập các cuốn sách §  Name = {(N0), (N1), (N2)} §  Addr = {(D0), (D1)} §  Book = {(B0), (B1)} v Một quan hệ nhị phân tên - địa chỉ §  Address = {(N0, D0),(N1, D1)} v Một quan hệ bộ ba sách - tên - địa chỉ §  Addr = {(B0, N0, D0), (B0, N1, D1), (B1, N1, D2)} v Một số scalar: §  myName = {(N0)}, yourName = {(N1)} §  myBook = {(B0)} 13 Nguyễn Thị Minh Tuyền Atom Tuple Đặc tả hình thức Quan hệ v Kích thước của một quan hệ là số tuple trong quan hệ v Bậc của một quan hệ là số nguyên tử trong mỗi tuple của quan hệ §  Quan hệ với bậc là 1, 2, 3 được gọi là quan hệ đơn phân, nhị phân và quan hệ bậc ba. §  Một quan hệ với bậc lớn hơn ba gọi là một đa quan hệ. v Ví dụ: §  Quan hệ với bậc =1 và kích thước = 1: §  myName={(N0)} §  Quan hệ với bậc =2 và kích thước = 3 §  Address = {(N0, D0), (N1, D1), (N2, D1)} 14 Nguyễn Thị Minh Tuyền Đặc tả hình thức Nội dung v Nguyên tử và quan hệ v Signature và Field v Các phép toán 15 Nguyễn Thị Minh Tuyền Đặc tả hình thức Signature và Field v Signature §  Mô tả thực thể cần suy luận (reason) §  Các tập hợp được định nghĩa trong signature là cố định (khái niệm liên quan đến các thao tác (operation) và các mô hình động (dynamic model)) v Field §  Định nghĩa mối quan hệ giữa các signature v Các ràng buộc đơn giản §  Multiplicity trên signature §  Multiplicity trên quan hệ 16 Nguyễn Thị Minh Tuyền Đặc tả hình thức Signature v Một signature khai báo một tập các nguyên tử. v Khai báo: §  sig A {} §  Khai báo một tập tên A. v Một tập có thể được khai báo như là một tập con của tập khác: §  sig A1 extends A {} §  Khai báo một tập A1 là tập con của A 17 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ abstract sig Person { children: set Person, siblings: set Person } sig Man, Woman extends Person {} sig Married in Person { spouse: one Married } 18 Nguyễn Thị Minh Tuyền Field Đặc tả hình thức Signature sig A {} sig B {} sig A1 extends A {} sig A2 extends A {} v A và B không giao nhau. v A1 và A2 là tập mở rộng của tập A. v A1 và A2 không giao nhau. (nhưng không phải A = A1∪A2). v Một signature được khai báo độc lập với các signature khác là top-level signature, ví dụ như A và B. v Các tập con của cùng một signature không giao nhau. 19 Nguyễn Thị Minh Tuyền B A1 A2 A Đặc tả hình thức abstract sig A {} sig B {} sig A1 extends A {} sig A2 extends A {} v Một signature có thể được khai báo như một tập con của một tập khác §  sig A3 in A {} v Một abstract signature không có phần tử nào ngoại trừ những phần tử đó thuộc về tập mở rộng hoặc tập con của nó. 20 Nguyễn Thị Minh Tuyền B A3 A A1 A2 Đặc tả hình thức abstract sig A {} sig B {} sig A1 extends A {} sig A2 extends A {} •  Ta có ba tập với các ràng buộc •  A1 in A và A2 in A •  Vì A1 và A2 mở rộng của A và •  A in A1 + A2 •  Vì A là abstract, do đó, •  A = A1 + A2 •  và A1 và A2 là tập phân hoạch từ A. 21 Nguyễn Thị Minh Tuyền B A3 A A1 A2 Đặc tả hình thức Ví dụ abstract sig Person {} sig Man extends Person {} sig Woman extends Person {} sig Married in Person {} 22 Nguyễn Thị Minh Tuyền Married Man Woman Married Person Man Woman in extends Extends Đặc tả hình thức v Một signature có thể được khai báo như là một tập con của tập hợp §  sig C in A + B {} §  Mỗi phần tử của C thuộc về A hoặc thuộc về B 23 Nguyễn Thị Minh Tuyền Đặc tả hình thức Instance của mô hình Person = {(P0),(P1),(P2)} Man = {(P1),(P2)} Married = {} Woman = {(P0),(P1)} Person = {(P0),(P1)} Man = {(P0)} Married = {(P1)} Woman = {} Person = {(P0),(P1),(P2)} Man = {(P1),(P2)} Married = {} Woman = {(P0)} Person = {(P0),(P1),(P2), (P3)} Man = {(P0),(P1),(P2), (P3)} Married = {(P2),(P3)} Woman = {} Person = {(P0),(P1)} Man = {(P0)} Married = {(P1),(P0)} Woman = {(P1)} 24 Nguyễn Thị Minh Tuyền abstract sig Person {} sig Man extends Person {} sig Woman extends Person {} sig Married in Person {} Đặc tả hình thức Field v Quan hệ được khai báo dưới dạng các field của các signature §  sig A{f: e} §  khai báo một quan hệ f mà miền của nó là A và ảnh của nó được đưa ra bởi e. v Ví dụ: §  quan hệ nhị phân: §  sig A {f1: A} // f1 là tập con của A x A §  quan hệ bậc 3: §  sig B {f2: A -> A} // f2 là tập con của B x A x A 25 Nguyễn Thị Minh Tuyền Đặc tả hình thức sibling là một quan hệ nhị phân. Nó là tập con của Person x Person Ví dụ abstract sig Person { siblings: Person } sig Man extends Person {} sig Woman extends Person {} sig Married in Person {} 26 Nguyễn Thị Minh Tuyền Person = {(P0), (P1)} Man = {(P0), (P1)} Married = {} Woman = {} siblings = {(P0,P1), (P1,P0)} P0 và P1 là sibling Đặc tả hình thức Multiplicity v  Cho phép ràng buộc kích thước tập hợp §  Từ khóa multiplicity được đặt trước một khai báo signature ràng buộc số phần tử trong tập hợp của signature. m sig A {} §  nghĩa là A có m phần tử §  Cũng có thể tạo ra các ràng buộc trên các field sig A {f: m e} sig A {f: e1 m -> n e2} v  Có 4 loại multiplicity §  set: bất kỳ số nào §  some: 1 hoặc nhiều §  lone: 0 hoặc 1 §  one: chính xác 1 27 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ v Không có multiplicity: §  Một tập các điểm ảnh, mỗi điểm ảnh có màu hoặc đỏ, hoặc xanh lá cây, hoặc xanh da trời. abstract sig Pixel{} sig Red, Green, Blue extends Pixel{} v Với multiplicity §  Một liệt kê về màu đèn giao thông abstract sig Color{} one sig Red, Yellow, Green extends Color{} 28 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ v Một hệ thống file trong đó mỗi đường dẫn chứa một số các đối tượng, mỗi một alias chỉ chính xác đến một đối tượng. abstract sig Object {} sig Dir extends Object {contents: set Object} sig File extends Object {} sig Alias in File {to: one Object} sig Temp in File + Dir {} v Từ khóa mặc định, nếu bỏ qua là one. Vì vậy §  sig A {f: e} và sig A {f: one e} tương đương nhau. 29 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ v Một cuốn sách ánh xạ tên thành địa chỉ v Có nhiều nhất một địa chỉ/tên v Một địa chỉ liên quan đến ít nhất một tên sig Name, Addr {} sig Book { addr: Name some -> lone Addr } 30 Nguyễn Thị Minh Tuyền Đặc tả hình thức v Một tập các dự báo thời tiết, mỗi một dự báo có một field weather liên quan đến một thành phố với chính xác một điều kiện thời tiết. sig Forecast {weather: City -> one Weather} sig City {} abstract sig Weather {} one sig Rainy, Sunny, Cloudy extends Weather {} v Instance: City = {(Iowa City), (Chicago)} Rainy = {(rainy)} Sunny = {(sunny)} Cloudy = {(cloudy)} Forecast = {(f1), (f2)} weather = { (f1, Iowa City, rainy), (f1, Chicago, rainy), (f2, Iowa City, rainy), (f2, Chicago, sunny) } 31 Nguyễn Thị Minh Tuyền Đặc tả hình thức Multiplicity và quan hệ nhị phân sig S {f: lone T} v với mỗi phần tử s của S, f ánh xạ s thành nhiều nhất một giá trị trong T 32 Nguyễn Thị Minh Tuyền A s1 t1 s2 t2 s3 t3 s4 t4 B s1 t1 s2 t2 s3 t3 s4 t4 C s1 t1 s2 t2 s3 t3 s4 t4 D s1 t1 s2 t2 s3 t3 s4 t4 Đặc tả hình thức Multiplicity và quan hệ bậc 3 sig S {f: T -> one V} v với mỗi phần tử s của S, field f thỏa mãn: với mỗi phần tử t của T, f ánh xạ t vào chính xác một giá trị trong V 33 Nguyễn Thị Minh Tuyền A s1 t1 v1 t2 v2 t3 v3 t4 v4 B s1 s2 t1 v1 t2 v2 t3 v3 t4 v4 C s1 s2 t1 v1 t2 v2 t3 v3 t4 v4 D s1 s1 t1 s2 t2 s3 t3 s4 t4 Đặc tả hình thức Multiplicity và quan hệ v Các loại khác của cấu trúc quan hệ có thể được đặc tả sử dụng multiplicity. v Ví dụ: §  sig S {f: some T} total relation §  sig S {f: set T} partial relation §  sig S {f: T set -> set V} §  sig S {f: T one -> V} §  ... 34 Nguyễn Thị Minh Tuyền Đặc tả hình thức Các ký hiệu trong Alloy 35 Nguyễn Thị Minh Tuyền A+ some sig A {} A abstract abstract sig A {} A lone sig A {} A sig A {} A A1 sig A {} sig A1 extends A {} A A1 sig A {} sig A1 in A {} in Đặc tả hình thức Ví dụ: Cấu trúc gia đình v Sử dụng multiplicity để định nghĩa quan hệ children như thế nào? sig Person {children: set Person} §  Dễ thấy, mỗi người có 0 hoặc nhiều con v Làm sao định nghĩa quan hệ spouse sử dụng multiplicity? sig Married {spouse: one Married} §  Mỗi người đã kết hôn có chính xác một vợ/chồng. 36 Nguyễn Thị Minh Tuyền Đặc tả hình thức Tóm tắt v Mô hình Alloy abstract sig Person { children: set Person, siblings: set Person } sig Man, Woman extends Person {} sig Married in Person { spouse: one Married } 37 Nguyễn Thị Minh Tuyền Đặc tả hình thức Model Instance Person = {Man0,Man1,Man2} Man = {Man0,Man1,Man2} Woman = {} Married = {Man0,Man1,Man2} children = { (Man0,Man0),(Man0,Man1), (Man1,Man0), (Man2,Man1), (Man2,Man2) } siblings = { (Man0,Man0),(Man0,Man1), (Man1,Man0),(Man1,Man2), (Man2,Man2) } spouse = {(Man1,Man0),(Man0,Man2),(Man2,Man0)} 38 Nguyễn Thị Minh Tuyền Đặc tả hình thức Một người có thể là con của chính họ ? Person = {Man0,Man1,Man2} Man = {Man0,Man1,Man2} Woman = {} Married = {Man0,Man1,Man2} children = { (Man0,Man0),(Man0,Man1), (Man1,Man0), (Man2,Man1), (Man2,Man2) } siblings = { (Man0,Man0),(Man0,Man1), (Man1,Man0),(Man1,Man2), (Man2,Man2) } spouse = {(Man1,Man0),(Man0,Man2),(Man2,Man0)} 39 Nguyễn Thị Minh Tuyền Đặc tả hình thức Nhiều cha Person = {Man0,Man1,Man2} Man = {Man0,Man1,Man2} Woman = {} Married = {Man0,Man1,Man2} children = { (Man0,Man0),(Man0,Man1), (Man1,Man0), (Man2,Man1), (Man2,Man2) } siblings = { (Man0,Man0),(Man0,Man1), (Man1,Man0),(Man1,Man2), (Man2,Man2) } spouse = {(Man1,Man0),(Man0,Man2),(Man2,Man0)} 40 Nguyễn Thị Minh Tuyền Đặc tả hình thức Một người là anh chị em của chính họ? Person = {Man0,Man1,Man2} Man = {Man0,Man1,Man2} Woman = {} Married = {Man0,Man1,Man2} children = { (Man0,Man0),(Man0,Man1), (Man1,Man0), (Man2,Man1), (Man2,Man2) } siblings = { (Man0,Man0),(Man0,Man1), (Man1,Man0),(Man1,Man2), (Man2,Man2) } spouse = {(Man1,Man0),(Man0,Man2),(Man2,Man0)} 41 Nguyễn Thị Minh Tuyền Đặc tả hình thức Vừa là con vừa là anh chị em? Person = {Man0,Man1,Man2} Man = {Man0,Man1,Man2} Woman = {} Married = {Man0,Man1,Man2} children = { (Man0,Man0),(Man0,Man1), (Man1,Man0), (Man2,Man1), (Man2,Man2) } siblings = { (Man0,Man0),(Man0,Man1), (Man1,Man0),(Man1,Man2), (Man2,Man2) } spouse = {(Man1,Man0),(Man0,Man2),(Man2,Man0)} 42 Nguyễn Thị Minh Tuyền Đặc tả hình thức Không đối xứng? Person = {Man0,Man1,Man2} Man = {Man0,Man1,Man2} Woman = {} Married = {Man0,Man1,Man2} children = { (Man0,Man0),(Man0,Man1), (Man1,Man0), (Man2,Man1), (Man2,Man2) } siblings = { (Man0,Man0),(Man0,Man1), (Man1,Man0),(Man1,Man2), (Man2,Man2) } spouse = {(Man1,Man0),(Man0,Man2),(Man2,Man0)} “(Man0,Man1) ?” 43 Nguyễn Thị Minh Tuyền Đặc tả hình thức Điểm yếu của mô hình v Ràng buộc trong mô hình kém v Ta có thể thêm các ràng buộc vào mô hình. v Các mô hình được ràng buộc kém là điểm chung trong giai đoạn đầu của qui trình phát triển. v AA cho ta một phản hồi nhanh chóng về điểm yếu trong mô hình. v Ta có thể thêm dần dần các ràng buộc cho đến khi nào được thỏa mãn. 44 Nguyễn Thị Minh Tuyền Đặc tả hình thức Thêm ràng buộc v Thêm các ràng buộc sau §  Ràng buộc về mặt sinh học •  Không ai có thể là bố mẹ của chính họ •  Không ai có nhiều hơn một bố hoặc mẹ •  Anh chị em của một người là những người có cùng bố mẹ §  Ràng buộc về mặt xã hội •  Một quan hệ vợ chồng là đối xứng •  Vợ của một người đàn ông không thể là một trong các chị em của ông ta. 45 Nguyễn Thị Minh Tuyền Đặc tả hình thức Nội dung v Nguyên tử và quan hệ v Signature và Field v Các phép toán 46 Nguyễn Thị Minh Tuyền Đặc tả hình thức Các tập được định nghĩa trước v Có ba hằng số §  none tập rỗng (không chứa nguyên tử nào). §  univ tập universal (là tập trong đó mọi nguyên tử là nguyên phân). §  ident identity (là quan hệ nhị phân, chứa các tuple trong đó ánh xạ mỗi atom thành chính nó). v Ví dụ: §  cho một mô hình chỉ với hai tập Name = {(N0),(N1),(N2)} Addr = {(D0),(D1)} §  các hằng số có giá trị •  none = {} •  univ = {(N0),(N1),(N2),(D0),(D1)} •  ident ={(N0,N0),(N1,N1),(N2,N2),(D0,D0),(D1,D1)} 47 Nguyễn Thị Minh Tuyền Đặc tả hình thức Phép lượng hóa (Quantifier) v Alloy có các quantifier sau §  all x: S | F F đúng cho mọi x trong S §  some x: S | F F đúng cho một số giá trị của x trong S §  no x: S | F F sai với mọi giá trị x trong S §  lone x: S | F F đúng cho nhiều nhất một giá trị trong S §  one x: S | F F đúng cho chính xác một giá trị x trong S v Quantifier có thể được áp dụng để biểu diễn §  some e e không rỗng §  no e e rỗng §  lone e e có nhiều nhất một tuple §  one e e có chính xác một tuple v Chú ý: some e và no e có thể được viết v e!=none và e = none 48 Nguyễn Thị Minh Tuyền Đặc tả hình thức Ví dụ v some Name §  tập hợp các tên không rỗng v some address §  các địa chỉ không rỗng: có một số cặp ánh xạ từ tên thành địa chỉ v no (address.Addr – Name) §  không có gì được ánh xạ tới địa chỉ trừ tên v all n:Name|lone n.address §  tất cả các tên ánh xạ đến nhiều nhất một địa chỉ 49 Nguyễn Thị Minh Tuyền Đặc tả hình thức Phép toán tập hợp v Các phé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