›

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

pdf 69 trang huongle 2140
Download
Bạn đang xem 20 trang mẫu của tài liệu "Giáo trình Đặc tả hình thức - Chương 3: Giới thiệu về Alloy - Nguyễn Thị Minh Tuyền", để tải tài liệu gốc về máy bạn click vào nút DOWNLOAD ở trên

Tài liệu đính kèm:

  • pdfgiao_trinh_dac_ta_hinh_thuc_chuong_3_gioi_thieu_ve_alloy_ngu.pdf

Nội dung text: Giáo trình Đặc tả hình thức - Chương 3: 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. Nội dung v Nguyên tử và quan hệ v Signature và Field v Các phép toán Nguyễn Thị Minh Tuyền 2 Đặc tả hình thức
  3. 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: § Nguyễn Thị Minh Tuyền 3 Đặc tả hình thức
  4. 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. Nguyễn Th ị Minh Tuyền 4 Đặc tả hình thức
  5. 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 Nguyễn Thị Minh Tuyền 5 Đặc tả hình thức
  6. 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. Nguyễn Thị Minh Tuyền 6 Đặc tả hình thức
  7. 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ả. Nguyễn Thị Minh Tuyền 7 Đặc tả hình thức
  8. 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) Nguyễn Thị Minh Tuyền 8 Đặc tả hình thức
  9. 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. FriendBook Ted -> ted@gmail.com Ryan -> ryan@hotmail.com WorkBook Pilard -> pilard@hcmus.edu.vn Ryan -> ryan@hcmus.edu.vn Nguyễn Thị Minh Tuyền 9 Đặc tả hình thức
  10. Nội dung v Nguyên tử và quan hệ v Signature và Field v Các phép toán Nguyễn Thị Minh Tuyền 10 Đặc tả hình thức
  11. 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ử. Nguyễn Thị Minh Tuyền 11 Đặc tả hình thức
  12. 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. Nguyễn Thị Minh Tuyền 12 Đặc tả hình thức
  13. 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)} Atom § Book = {(B0), (B1)} Tuple 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)} Nguyễn Thị Minh Tuyền 13 Đặc tả hình thức
  14. 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)} Nguyễn Thị Minh Tuyền 14 Đặc tả hình thức
  15. Nội dung v Nguyên tử và quan hệ v Signature và Field v Các phép toán Nguyễn Thị Minh Tuyền 15 Đặc tả hình thức
  16. 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ệ Nguyễn Thị Minh Tuyền 16 Đặc tả hình thức
  17. 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 Nguyễn Thị Minh Tuyền 17 Đặc tả hình thức
  18. Ví dụ abstract sig Person { children: set Person, siblings: set Person Field } sig Man, Woman extends Person {} sig Married in Person { spouse: one Married } Nguyễn Thị Minh Tuyền 18 Đặc tả hình thức
  19. Signature sig A {} A1 sig B {} A2 A sig A1 extends A {} sig A2 extends A {} B 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. Nguyễn Thị Minh Tuyền 19 Đặc tả hình thức
  20. abstract sig A {} A1 A2 A sig B {} A3 sig A1 extends A {} sig A2 extends A {} B 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ó. Nguyễn Thị Minh Tuyền 20 Đặc tả hình thức
  21. abstract sig A {} A1 A2 A sig B {} A3 sig A1 extends A {} sig A2 extends A {} B • 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. Nguyễn Thị Minh Tuyền 21 Đặc tả hình thức
  22. Ví dụ abstract sig Person {} sig Man extends Person {} Married sig Woman extends Person {} sig Married in Person {} in Person Man Woman Married extends Extends Man Woman Nguyễn Thị Minh Tuyền 22 Đặc tả hình thức
  23. 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 Nguyễn Thị Minh Tuyền 23 Đặc tả hình thức
  24. Instance của mô hình abstract sig Person {} sig Man extends Person {} sig Woman extends Person {} sig Married in Person {} Person = {(P0),(P1),(P2)} Person = {(P0),(P1)} Man = {(P1),(P2)} Man = {(P0)} Married = {} Married = {(P1)} Woman = {(P0),(P1)} Woman = {} Person = {(P0),(P1),(P2)} Person = {(P0),(P1),(P2), Person = {(P0),(P1)} Man = {(P1),(P2)} (P3)} Man = {(P0)} Married = {} Man = {(P0),(P1),(P2), Married = {(P1),(P0)} Woman = {(P0)} (P3)} Woman = {(P1)} Married = {(P2),(P3)} Woman = {} Nguyễn Thị Minh Tuyền 24 Đặc tả hình thức
  25. 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 Nguyễn Thị Minh Tuyền 25 Đặc tả hình thức
  26. Ví dụ abstract sig Person { Person = {(P0), (P1)} siblings: Person Man = {(P0), (P1)} Married = {} } Woman = {} sig Man extends Person {} sig Woman extends Person {} siblings = {(P0,P1), (P1,P0)} sig Married in Person {} sibling là một quan hệ nhị phân. Nó là tập con của Person x Person P0 và P1 là sibling Nguyễn Thị Minh Tuyền 26 Đặc tả hình thức
  27. 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 Nguyễn Thị Minh Tuyền 27 Đặc tả hình thức
  28. 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{} Nguyễn Thị Minh Tuyền 28 Đặc tả hình thức
  29. 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. Nguyễn Thị Minh Tuyền 29 Đặc tả hình thức
  30. 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 } Nguyễn Thị Minh Tuyền 30 Đặc tả hình thức
  31. 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) } Nguyễn Thị Minh Tuyền 31 Đặc tả hình thức
  32. 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 A s1 t1 B s1 t1 C s1 t1 D s1 t1 s2 t2 s2 t2 s2 t2 s2 t2 s3 t3 s3 t3 s3 t3 s3 t3 s4 t4 s4 t4 s4 t4 s4 t4 Nguyễn Thị Minh Tuyền 32 Đặc tả hình thức
  33. 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 A t1 v1 B t1 v1 C t1 v1 D s1 t1 t2 v2 t2 v2 t2 v2 s2 t2 s1 s1 s1 s1 t3 v3 t3 v3 t3 v3 s3 t3 t4 v4 s2 t4 v4 s2 t4 v4 s4 t4 Nguyễn Thị Minh Tuyền 33 Đặc tả hình thức
  34. 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} § Nguyễn Thị Minh Tuyền 34 Đặc tả hình thức
  35. Các ký hiệu trong Alloy A A A+ abstract sig A {} some sig A {} abstract sig A {} A A A lone sig A {} in A1 A1 sig A {} sig A {} sig A1 extends A {} sig A1 in A {} Nguyễn Thị Minh Tuyền 35 Đặc tả hình thức
  36. 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. Nguyễn Thị Minh Tuyền 36 Đặc tả hình thức
  37. 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 } Nguyễn Thị Minh Tuyền 37 Đặc tả hình thức
  38. 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)} Nguyễn Thị Minh Tuyền 38 Đặc tả hình thức
  39. 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)} Nguyễn Thị Minh Tuyền 39 Đặc tả hình thức
  40. 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)} Nguyễn Thị Minh Tuyền 40 Đặc tả hình thức
  41. 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)} Nguyễn Thị Minh Tuyền 41 Đặc tả hình thức
  42. 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)} Nguyễn Thị Minh Tuyền 42 Đặc tả hình thức
  43. 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) ?” Nguyễn Thị Minh Tuyền 43 Đặc tả hình thức
  44. Đ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. Nguyễn Thị Minh Tuyền 44 Đặc tả hình thức
  45. 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. Nguyễn Thị Minh Tuyền 45 Đặc tả hình thức
  46. Nội dung v Nguyên tử và quan hệ v Signature và Field v Các phép toán Nguyễn Thị Minh Tuyền 46 Đặc tả hình thức
  47. 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)} Nguyễn Thị Minh Tuyền 47 Đặc tả hình thức
  48. 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 Nguyễn Thị Minh Tuyền 48 Đặc tả hình thức
  49. 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ỉ Nguyễn Thị Minh Tuyền 49 Đặc tả hình thức
  50. 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 Nguyễn Thị Minh Tuyền 50 Đặc tả hình thức
  51. 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 Nguyễn Thị Minh Tuyền 51 Đặc tả hình thức
  52. 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. Nguyễn Thị Minh Tuyền 52 Đặc tả hình thức
  53. Phép toán quan hệ § -> arrow (product) § ~ chuyển vị § . dot join § [] box join § ^ transitive closure § * reflexive-transitive closure § giới hạn ảnh (image restriction) § ++ override Nguyễn Thị Minh Tuyền 53 Đặc tả hình thức
  54. 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ó. Nguyễn Thị Minh Tuyền 54 Đặc tả hình thức
  55. 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 Nguyễn Thị Minh Tuyền 55 Đặc tả hình thức
  56. 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. Nguyễn Thị Minh Tuyền 56 Đặc tả hình thức
  57. 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)} Nguyễn Thị Minh Tuyền 57 Đặc tả hình thức
  58. 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)} Nguyễn Thị Minh Tuyền 58 Đặc tả hình thức
  59. 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ể. Nguyễn Thị Minh Tuyền 59 Đặc tả hình thức
  60. Ví dụ v to: ánh xạ một message thành tên mà M0 N0 D0 nó định gởi đến. v address: ánh xạ tên thành địa chỉ. M1 N1 D1 § to = {(M0,N0),(M0,N2), (M1,N2),(M2,N3)} § address = {(N0,D0), M2 N2 D3 (N0,D1),(N1,D1),(N2,D3)} v to.address ánh xạ message thành địa chỉ mà nó định gởi N3 § to.address = {(M0,D0), to (M0,D1),(M0,D3),(M1,D3)} address Nguyễn Thị Minh Tuyền 60 Đặc tả hình thức
  61. 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 Nguyễn Thị Minh Tuyền 61 Đặc tả hình thức
  62. 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 Nguyễn Thị Minh Tuyền 62 Đặc tả hình thức
  63. 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+ Nguyễn Thị Minh Tuyền 63 Đặc tả hình thức
  64. 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à: address G0 A0 D0 ^address - address 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)} Nguyễn Thị Minh Tuyền 64 Đặc tả hình thức
  65. 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) Nguyễn Thị Minh Tuyền 65 Đặc tả hình thức
  66. 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ụ: (S0,S1) (S1,S2) (S2,S3) (S0,S1) ^r (S1,S2) (S4,S7) (S2,S3) (S0,S2) (S4,S7) (S0,S3) (S1,S3) *r r (S0,S0) (S1,S1) (S2,S2) (S3,S3) (S4,S4) (S7,S7) Nguyễn Thị Minh Tuyền 66 Đặc tả hình thức
  67. 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 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 Man = {(M0,M1),(M0,M2),(W1,M1)}// parent-son Nguyễn Thị Minh Tuyền 67 Đặc tả hình thức
  68. 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)} Nguyễn Thị Minh Tuyền 68 Đặc tả hình thức