Bài giảng Đặc tả hình thức: Chương 3

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

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:

§  http://alloy.mit.edu/alloy/

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 Đặc tả hình thức Nguyễn Thị Minh Tuyền

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.

FriendBook

Ted -> ted@gmail.com

Ryan -> ryan@hotmail.com

WorkBook

Pilard -> pilard@hcmus.edu.vn

Ryan -> ryan@hcmus.edu.vn

9 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

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ụ

Atom

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)}

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)}

13 Nguyễn Thị Minh Tuyền Đặ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 {

Field

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 Đặ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 Đặ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 Đặ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 Đặc tả hình thức

Ví dụ

Married

abstract sig Person {} sig Man extends Person {} sig Woman extends Person {} sig Married in Person {}

Person

Man

Woman

extends

Extends

Married

Man

Woman

22 Nguyễn Thị Minh Tuyền Đặ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

abstract sig Person {} sig Man extends Person {} sig Woman extends Person {} sig Married in Person {}

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)} Man = {(P0)} Married = {(P1),(P0)} Woman = {(P1)}

Person = {(P0),(P1),(P2), (P3)} Man = {(P0),(P1),(P2), (P3)} Married = {(P2),(P3)} Woman = {}

24 Nguyễn Thị Minh Tuyền Đặ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

Ví dụ

abstract sig Person { siblings: Person

Person = {(P0), (P1)} Man = {(P0), (P1)} Married = {} Woman = {} siblings = {(P0,P1), (P1,P0)}

} sig Man extends Person {} sig Woman extends Person {} 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

26 Nguyễn Thị Minh Tuyền Đặ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

A s1

B s1

C s1

D s1

32 Nguyễn Thị Minh Tuyền Đặ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

D s1

A s1

B s1 s2

C s1 s2

33 Nguyễn Thị Minh Tuyền Đặ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ụ:

…total relation …partial relation

§  sig S {f: some T} §  sig S {f: set T} §  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

A+

A abstract

sig A {}

some sig A {}

abstract sig A {}

lone sig A {}

sig A {} sig A1 extends A {}

sig A {} sig A1 in A {}

35 Nguyễn Thị Minh Tuyền Đặ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 {

(Man0,Man0),(Man0,Man1), (Man1,Man0),(Man1,Man2), (Man2,Man2)

= {(Man1,Man0),(Man0,Man2),(Man2,Man0)}

} spouse “(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ố

tập rỗng (không chứa nguyên tử nào). tập universal (là tập trong đó mọi nguyên tử là nguyên

§  none §  univ

identity (là quan hệ nhị phân, chứa các tuple trong đó

§

phân). ident á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

= {(N0),(N1),(N2)} = {(D0),(D1)}

Name Addr §  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

F đúng cho mọi x trong S F đúng cho một số giá trị của x trong S F sai với mọi giá trị x trong S F đúng cho nhiều nhất một giá trị trong S 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 §  no e §  lone e §  one e

e không rỗng e rỗng e có nhiều nhất một tuple 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 tập con bằng nhau

§  + §  & §  - §  in §  =

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

Đặ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

= {(D0),(D1)}

= {(N0),(N1)} = {(B0)}

= {(N0,D0),(N0,D1),(N1,D0),(N1,D1)}

Addr Book Name -> Addr 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),

to address

(M0,D1),(M0,D3),(M1,D3)}

60 Nguyễn Thị Minh Tuyền Đặ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à:

address

^address - address

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)}

64 Nguyễn Thị Minh Tuyền Đặ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ụ:

^r

(S0,S1) (S1,S2) (S2,S3) (S4,S7)

*r

r

(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)

66 Nguyễn Thị Minh Tuyền Đặ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 Đặc tả hình thức

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