Chương V: Đặc tả với ngôn ngữ Z

Ch

ng V: Đ c t

v i ngôn ng Z

Đ c t

Hình th c

ươ

ặ ả ớ

ữ

Bài gi ng môn ả

ặ ả

ứ

NGÔN NG Đ C T Z

Ữ Ặ

Ả

CH NG V: ƯƠ ng: c a ch Các n i dung chính ươ ủ

ộ

CH 1 NG V: NGÔN NG Đ C T Z ................................................................................... ƯƠ Ữ Ặ Ả

V.1 Gi ớ 3 i thi u ....................................................................................................................... ệ

V.2 Các thành ph n c a ngôn ng ầ ủ 3 ........................................................................................ ữ

3 V.2.1 Logic toán h cọ ........................................................................................................

V.2.1.1 Logic m nh đệ 3 .................................................................................................. ề

3 V.2.1.2 Logic v tị ừ .........................................................................................................

5 V.2.2 Lý thuy t t p h p .................................................................................................. ợ ế ậ

6 V.2.3 Hàm và quan hệ .....................................................................................................

6 V.2.3.1 Quan h 2 ngôi .................................................................................................. ệ

6 .......................................................................... V.2.3.2 Mi n xác đ nh và mi n giá tr ị ị ề ề

6 V.2.3.3 Hàm ...................................................................................................................

6 V.2.3.4 Hàm riêng ph nầ .................................................................................................

6 V.2.3.5 Hàm toàn ph nầ ..................................................................................................

7 V.3 Gi n đ (schemas) .......................................................................................................... ồ ả

V.3.1 Gi 7 i thi u chung .................................................................................................... ớ ệ

7 V.3.2 Đ nh nghĩa .............................................................................................................. ị

V.3.3 Toán t 8 đ t tên ....................................................................................................... ử ặ

V.3.4 Gi n đ t ng đ 8 ng ........................................................................................... ồ ươ ả ươ

8 V.3.5 M t s ghi chú ...................................................................................................... ộ ố

V.3.6 Gi n đ đ ồ ượ ử ụ 9 c s d ng nh 1 ki u d li u ......................................................... ể ữ ệ ư ả

V.3.7 Gi n đ đ 10 c s d ng trong các khai báo ......................................................... ồ ượ ử ụ ả

V.3.8 Gi n đ đ c s d ng trong các bi u th c l ng t ồ ượ ử ụ ứ ượ ể ả 11 ....................................... ừ

V.3.9 Gi n đ đ c s d ng nh 1 v t ồ ượ ử ụ 11 .................................................................... ị ừ ư ả

V.3.10 D ng chu n c a 1 gi n đ ẩ ủ ạ ả 12 ............................................................................... ồ

V.3.11 Đ t l i tên các thành ph n trong gi n đ ặ ạ ả ầ 13 ......................................................... ồ

V.4 Các phép toán trên gi n đả 13 ........................................................................................... ồ

13 V.4.1 Phép n i li n (Conjunction) ................................................................................. ố ề

14 V.4.2 Phép đ i tên (Decoration) .................................................................................... ổ

15 V.4.3 Phép n i r i (Disjunction) ................................................................................... ố ờ

15 V.4.4 Phép ph đ nh (Negation) .................................................................................... ủ ị

1 Biên so n: Nguy n Tr n Thi Văn ễ

ầ

ạ

Ch

ng V: Đ c t

v i ngôn ng Z

Đ c t

Hình th c

ươ

ặ ả ớ

ữ

Bài gi ng môn ả

ặ ả

ứ

V.4.5 Phép l ng t 16 hóa ............................................................................................... ượ ừ

17 V.5 Bài t p áp d ng ............................................................................................................. ậ ụ

2 Biên so n: Nguy n Tr n Thi Văn ễ

ầ

ạ

Ch

ng V: Đ c t

v i ngôn ng Z

Đ c t

Hình th c

ươ

ặ ả ớ

ữ

Bài gi ng môn ả

ặ ả

ứ

V.1 Gi

ớ

c g i là ngôn ng Z đ ượ ượ ữ ọ ự ặ ữ c s d ng ch các yêu c u ch c năng c a 1 h th ng, đ c bi hình th c đ đ c t c xây d ng d a trên lý thuy t t p ế ậ ủ ệ t ự ẽ ượ ử ụ ặ ệ ố ứ ể ặ ả ọ ứ ủ ầ

i thi u ệ Ký pháp Z, hay còn đ h p và logic toán h c. Đây là m t ngôn ng toán h c ch t ch , đ ộ ọ ợ y u trong đ c t ặ ả ế là h th ng ph n m m. ầ

ệ ố ề

t k đ mô t ượ ủ ệ ố ế ế ể ầ ụ ụ c thi các yêu c u phi ch c năng c a h th ng, ứ ữ c hay đ tin c y c a h th ng. Ngôn ng ậ ủ ệ ố ố theo th i gian hay x lý song song. Mu n ử c thi ệ ế ế ộ ờ ượ ả ướ ặ ả c đi u này, ta ph i k t h p Z cùng v i các công c khác n a. Ngôn ng Z không đ ữ ví d nh công d ng, hi u năng, kích th ư cũng không đ t k cho các đ c t làm đ ề ượ ả ế ợ ụ ữ ớ

V.2 Các thành ph n c a ngôn ng

ầ ủ

ữ

V.2.1 Logic toán h cọ

V.2.1.1 Logic m nh đệ

ề

ệ ư ệ ố ệ ề ệ ề

ủ ọ ữ ề ố ớ Các khái ni m v logic m nh đ cũng nh h th ng ký hi u c a logic m nh đ trong ký pháp Z hoàn toàn gi ng v i ngôn ng toán h c thông th ng. ệ ườ

c li t kê trong b ng d ệ ề ệ ả ướ i Có 5 phép toán m nh đ trong ngôn ng Z đ trên xu ng d đây, v i đ u tiên gi m d n t ả ớ ộ ư ầ ừ ữ ố ượ ướ : i

Phép toán (cid:216)

(cid:217)

(cid:218)

(cid:222)

(cid:219) T ng Ý nghĩa Ph đ nh ủ ị Tuy nể H iộ Kéo theo ng đ ươ ươ

ơ ở ng 2 (Các c s t n a. i chi ti Ý nghĩa c a m i phép toán đã đ ượ ỗ ủ c a đ c t ). Do v y, ph n này xin đ ậ ủ ặ ả ầ c trình bày trong Ch ượ ươ c phép không nh c l ắ ạ ế ữ

V.2.1.2 Logic v tị ừ

cũng hoàn toàn gi ng nh trong ủ ệ ư ố Các khái ni m và đ nh nghĩa c a logic v t ị toán h c, ngo i tr ký hi u có khác bi ị ừ t. ạ ừ ệ ệ ọ

s d ng l ng t : ị ừ ử ụ ượ ừ

a) Cú pháp chung c a 1 v t ủ Q x : A | p • q

Trong đó:

). ng t ho c ặ "

ừ $ Q : l ( ượ x : bi n ràng bu c. ộ ế A : t p các giá tr c a x. ị ủ ậ p : ràng bu c trên bi n. ế ộ q : v t . ị ừ

3 Biên so n: Nguy n Tr n Thi Văn ễ

ầ

ạ

Ch

ng V: Đ c t

v i ngôn ng Z

Đ c t

Hình th c

ươ

ặ ả ớ

ữ

Bài gi ng môn ả

ặ ả

ứ

c phát bi u nh sau: “T n t ư ồ ạ ể ộ ề ậ i 1 giá tr x thu c v t p ị ượ

ộ ề ậ c phát bi u nh sau: “V i m i giá tr x thu c v t p ư ể ớ ọ ị ượ

$ x : A | p • q đ A, sao cho x th a p thì ta có q”. ỏ " x : A | p • q đ A, sao cho x th a p thì ta có q”. ỏ

•

Ta có các phát bi u t ể ươ ươ ng nh sau: ư

| qpAx

pAx

•

ng đ • (cid:217) $ (cid:219) $

| qpAx

pAx

(cid:222) " (cid:219) "

>•

“T n t i 1 s t c vi t nh sau trong ị ừ ồ ạ ố ự nhiên x l n h n 5” đ ớ ơ ượ ế ư Ví d 1ụ : V t ký pháp Z:

xNx

ư ậ ấ ấ ậ ợ

ệ nh trong toán h c. ư ộ ề ọ

ử ụ ứ ệ ạ ấ

•). Nh v y, ký hi u thu c v 1 t p h p trong Z là d u hai ch m (:), thay vì là d u ấ ˛ ử ụ Ký hi u “sao cho” s d ng d u g ch đ ng ( | ), và ký hi u “thì” s d ng ệ d u ch m tròn ( ấ ấ

ươ ọ " “v i m i” ớ ọ . “V i m i y ớ Ví d 2ụ : T thu c v t p s t nh th đ i v i l ớ

yNy

ng t ng t ư ế ố ớ ượ ự ừ nhiên, y l n h n hay b ng 0”. ằ ơ ộ ề ậ ố ự • ‡ "

b) “T n t ồ ạ ệ đ i ít nh t 2 giá tr th a đi u ki n” ị ỏ ề ấ ượ c bi u di n nh sau: ễ ư ể

, xAyx :

)

• qp

(cid:217) „ $

•

“T n t ồ ạ ệ đ i duy nh t 1 giá tr th a đi u ki n” ị ỏ ề ấ ượ c bi u di n nh sau: ễ ư ể

| qpAx

ể ấ ượ ễ c bi u di n ể i d ng v t Ví d 3ụ : Phát bi u “có duy nh t 1 quy n sách trên bàn” đ d ướ ạ

Desk

(

Books

)

(

Books

Desk

=• c

)

x ˛

Desk

˛ " (cid:217) $ ể nh sau: ị ừ ư ˛• b

ể ằ

có nghĩa là quy n sách x n m trên bàn.

ố ượ ệ ể

pAx

ấ ký pháp-m c) Ký pháp-m Đ xác đ nh đ i t ị dùng 1 ký pháp đ ng duy nh t trong t p h p th a đi u ki n, ngôn ng Z ữ ậ ề ỏ ợ , c th nh sau: c g i là ụ ể ư ượ ọ

m= (

pAx

)

và đ c đ c là: “có duy nh t 1 giá tr x thu c v t p A sao cho p” . ượ ọ ộ ề ậ ấ ị

t c là y là giá tr duy nh t thu c t p A sao ộ ậ ứ ấ ị

Khi ta ký hi u: ệ cho p đúng.

Nnm :

(

Ví d 4ụ : Ta nói “2 là s duy nh t thu c v t p s t ộ ề ậ ố ự ấ nhiên th a 4+n=6” ỏ

ố =+ n

4 Biên so n: Nguy n Tr n Thi Văn ễ

ầ

ạ

Ch

ng V: Đ c t

v i ngôn ng Z

Đ c t

Hình th c

ươ

ặ ả ớ

ữ

Bài gi ng môn ả

ặ ả

ứ

V.2.2 Lý thuy t t p h p

ế ậ ợ

ng t ự ươ ọ ở trên, các khái ữ ầ ợ ủ ữ ớ nh trong ph n Logic toán h c đã trình bày Cũng t ni m trong lý thuy t t p h p c a ngôn ng Z hoàn toàn gi ng v i ngôn ng ố ệ toán h c thông th ư ế ậ ng. ườ ọ

1. T p h p đ c bi u di n d i d ng li t kê : ợ ượ ậ ễ ướ ạ ể ệ

S == {a, b, c}

2. T p h p đ c bi u di n d i d ng v t ợ ượ ậ ễ ướ ạ ị ừ : ể

S == {x :X | p(x)}

3. T p h p r ng ợ ỗ : ậ

S == ˘

4. Đ bi u di n phát bi u ể : ‘giá tr x thu c v t p S’, ta dùng ký hi u ộ ề ậ ệ : ễ ị

ể ể x ˛ S

5. Đ bi u di n phát bi u ể : ‘giá tr x không thu c thu c v t p S’, ta dùng ề ậ ễ ộ ộ ị

ể ể ký hi uệ : S (cid:219) x ˇ (cid:216) (x ˛ S)

ậ

B = {x :U | x˛ A (cid:217) x˛ B}

˛ (cid:222) ˛ " (cid:219) (cid:204) : 6. Các phép toán trên t p h p ợ a. Giao : A ˙ b. H pợ : A ¨ B = {x :U | x˛ A (cid:218) x˛ B} c. Hi uệ : A \ B = {x :U | x˛ A (cid:217) xˇ B} d. T p con B Bx ậ

˛ (cid:222) ˛ " (cid:219) (cid:201) e. T p ch a trong : ứ ậ

= BA =

(cid:204) (cid:217) (cid:204) (cid:219) f. T p b ng nhau : ậ ằ

BAB

(cid:218) (cid:204) (cid:219) ˝ g.

BAB

(cid:218) ˚ (cid:219) ˚ h.

7. T p t t c các t p con c a 1 t p h p (Power set) ậ ấ ả ủ ậ ậ ợ

Ký hi uệ : P X

, {1}, {2}, {1, 2}} Ví dụ : X == {1, 2} P X = {˘

8. Tích Decartes c a 2 hay nhi u t p h p. ề ậ ủ ợ

5 Biên so n: Nguy n Tr n Thi Văn ễ

ầ

ạ

Ch

ng V: Đ c t

v i ngôn ng Z

Đ c t

Hình th c

ươ

ặ ả ớ

ữ

Bài gi ng môn ả

ặ ả

ứ

V.2.3 Hàm và quan hệ

i V.2.3.1 Quan h 2 ngô ệ

« Y là t p t t c các quan h 2 ngôi ậ ệ ợ ậ ấ ả ệ ế ữ

N u X, Y là các t p h p, ta ký hi u : X gi a X và Y. Ta có: X« Y == P(X· Y)

(x, y) trong đó x đ c l y t ỗ ộ ộ ứ ự ượ ấ ừ ậ t p M i ph n t X và y đ t p Y ầ ử ủ X« Y là m t b có th t c a c l y t ượ ấ ừ ậ

V.2.3.2 Mi n xác đ nh và mi n giá tr ị ị

ề ề

t c các giá ề c ký hi u là ệ ủ dom, là t p h p t ậ ợ ấ ả Mi n xác đ nh c a 1 quan h đ tr x thu c v t p X sao cho x có nh y thu c Y qua R. ệ ượ ả ộ ị

•

{

xYyXx

;

xRy }

ị ộ ề ậ = ˛ ˛ ˛ dom R

hay ta có th bi u di n theo 1 cách khác nh sau: ư ễ

•

xYy

Ry }

ể ể = ˛ $ dom R

t c các giá tr ề c ký hi u là ệ ệ ượ ị ran, là t p h p t ợ ấ ả ậ ộ ậ ủ ị

•

{

xYyXx

;

yRy }

Mi n giá tr c a quan h đ ị ủ c a y thu c v t p Y sao cho y là nh c a 1 giá tr x thu c t p X qua R. ả ộ ề ậ ủ = ˛ ˛ ˛ ran R

hay ta có th bi u di n theo 1 cách khác nh sau: ư ễ

•

xXx

Ry }

ể ể = ˛ $ ran R

V.2.3.3 Hàm

ậ ệ ầ ử ế ỗ ấ ệ ộ ậ c phân chia thành 2 lo i chính: hàm riêng ph n và hàm toàn ề thu c t p X có nhi u t p X đ n ế ừ ậ ượ ạ ầ Xét quan h R trên 2 t p h p X và Y, n u m i ph n t ộ ậ ợ nh t 1 nh y thu c t p Y qua R thì ta nói quan h R là 1 hàm đi t ả t p Y. Hàm đ ậ ph n.ầ

V.2.3.4 Hàm riêng ph nầ

ậ

ộ ế ị ầ ừ ậ ế ậ ˛ X thành nhi u nh t m t ề t p X đ n t p Y là 1 quan h trên t p X và t p Y, ậ ệ ˛ Y. Ký hi u:ệ ộ giá tr yị

xYyyXx ,

;

}

y 1

M t hàm riêng ph n t bi n m i giá tr x ỗ = = ấ • (cid:222) ˛ (cid:217) ˛ " « ﬁ ﬁ ﬁ

V.2.3.5 Hàm toàn ph nầ •

= =

dom o

}

ﬁ ﬁ

6 Biên so n: Nguy n Tr n Thi Văn ễ

ầ

ạ

Ch

ng V: Đ c t

v i ngôn ng Z

Đ c t

Hình th c

ươ

ặ ả ớ

ữ

Bài gi ng môn ả

ặ ả

ứ

V.3 Gi n đ (schemas) ồ

ả

V.3.1 Gi

i thi u chung

ớ

ệ

ữ ữ ữ ả ữ ọ ượ ử ụ các đ i t t k ữ ế ế : đ c t ặ ả ộ ồ ượ ả ế ợ Trong ngôn ng Z có 2 thành ph n ngôn ng chính ầ ng gi n đ . Ngôn ng toán h c đ ồ c a giai đo n thi ạ ủ quan h gi a chúng, v.v... Trong khi đó, ngôn ng gi n đ đ ệ ữ nên các b ng mô t ả th i đ t tên cho chúng đ s d ng l i : ngôn ng toán và ngôn c s d ng trong nhi u ph n khác nhau ầ ề ố các ràng bu c và m i ng, đ c t ố ượ ặ ả c dùng đ t o ể ạ ữ ả , k t h p, đóng gói các ph n thông tin khác nhau, đ ng ồ ầ ạ cho các m c đích khác. ụ ể ử ụ ờ ặ

ả ầ ặ ng nào đó là h t s c c n thi ế ứ ầ ử ụ t cho quá trình đ c t ặ ả ư ế ng n g n, chính xác, tránh trùng l p và rõ ràng, d hi u. Vi c đ nh nghĩa và đ t tên, cũng nh kh năng tái s d ng 1 thành ph n, 1 ị ệ đ i t . Nó giúp cho các ố ượ đ c t ặ ả ễ ể ắ ắ ọ

V.3.2 Đ nh nghĩa ị

i đ c t ườ ặ ả ị ủ ế ố ớ ồ ầ ữ ậ ư ấ đ nh nghĩa 1 khái Gi n đ (schema) là cú pháp c a Z cho phép ng ả ồ m i g m nhi u thành ph n thông tin khác nhau, có ràng bu c ni m, 1 y u t ộ ề ệ v i nhau, gi ng nh khái ni m c u trúc trong các ngôn ng l p trình; đ ng ồ ớ ệ ố th i đ t tên cho c u trúc này. ờ ặ ấ

ộ ả ế ầ ồ ị ừ ễ ả di n t Ta có th bi u di n m t gi n đ theo 1 ồ ồ ộ ữ ễ ả ộ ầ : ph n khai báo các bi n và ph n v t M t gi n đ bao g m 2 ph n ầ các ràng bu c trên nh ng bi n này. ể ể ế : trong 2 d ng sau ạ

 Theo chi u ngang : ề

[khai báo | ràng bu c]ộ

 Theo chi u d c ọ : ề

khai báo

ràng bu cộ

Ví dụ :

hay :

7 Biên so n: Nguy n Tr n Thi Văn ễ

ầ

ạ

Ch

ng V: Đ c t

v i ngôn ng Z

Đ c t

Hình th c

ươ

ặ ả ớ

ữ

Bài gi ng môn ả

ặ ả

ứ

V.3.3 Toán t

đ t tên

ử ặ

ằ

: , đ thu n l ệ ử ụ ể ặ ấ i sau này, ạ i cho ậ ợ ệ c ký hi u là i thành ệ ^= ồ ti n cho vi c s d ng l Nh m m c đích đ t tên cho 1 gi n đ , ả riêng, đ ngôn ng Z cung c p 1 toán t ượ t l c vi vi c so n th o, ký hi u này đ ế ạ ụ ữ ạ ử ượ ệ ệ ả

Tên ^= [khai báo | ràng bu c]ộ

Tên

khai báo

ràng bu cộ

Ví dụ :

hay :

V.3.4 Gi n đ t

ng đ

ng

ả ồ ươ

ươ

ng đ ng nhau n u chúng có cùng các bi n và ươ ươ ế Hai gi n đ đ ế ả có cùng ràng bu c gi ng nhau trên các bi n này. c g i là t ọ ố ồ ượ ộ ế

ng đ Ví dụ : 2 gi n đ sau đây là t ả ồ ươ ươ : ng

và

V.3.5 M t s g

ộ ố hi chú

ể ả ể ự ồ ơ ễ ọ ệ ả ắ  Đ gi n đ đ n gi n và d đ c h n, ta có th th c hi n ng t các khai ơ ả ượ c báo ra thành nhi u dòng khác nhau, m i khai báo trên 1 dòng và gi n l ề ỗ

8 Biên so n: Nguy n Tr n Thi Văn ễ

ầ

ạ

Ch

ng V: Đ c t

v i ngôn ng Z

Đ c t

Hình th c

ươ

ặ ả ớ

ữ

Bài gi ng môn ả

ặ ả

ứ

ẩ ; ) ngăn cách. Khi đó phép n i gi a các dòng này ữ ố ấ

các d u ch m ph y ( ấ m c nhiên là phép n i li n - ố ề ặ

(cid:217) (conjunction) ph n trên Ví dụ : gi n đ trong ví d ồ ụ ở ầ ả

có th đ c bi u di n l : ể ượ ễ ạ ể i nh sau ư

 N u 1 gi n đ đ n gi n ch khai báo các bi n mà không nêu ra ràng bu c ộ ả ả ỉ i đi. Ví d bên d ế c th trên các bi n này thì ta có th b ph n v t ụ ể ế ể ỏ ầ ồ ơ ế ị ừ ướ ụ :

ng đ : Khi đó, gi n đ s t ả ồ ẽ ươ ươ ng v i gi n đ sau ả ồ ớ

V.3.6 Gi n đ đ

ả ồ ượ ử ụ

c s d ng nh 1 ki u d li u ư

ể ữ ệ

ộ ữ ệ ể ậ ướ ủ ậ ể ử ụ ữ ệ ặ ồ ể c (N, Z, Q, Trong ngôn ng Z, m t ki u d li u có th là 1 t p cho tr ể ữ do ho c là 1 tích Decartes c a nhi u t p R, ...), 1 t p Power set, 1 ki u t ề ậ ể ự ặ h p. Ngoài ra, ta có th s d ng gi n đ nh 1 ki u d li u, sau khi đã đ t ư ả ợ tên cho gi n đ đó b ng phép toán đ t tên ^=. ặ ả ằ ồ

Ví d ta có gi n đ ụ ả ồ :

Nh v y khi khai báo : ư ậ

s : SchemaOne

thu c ki u SchemaOne, s s bao g m 2 thành ầ ử ế ồ ộ t cứ là s là m t bi n, 1 ph n t ẽ ộ ph n: a là 1 s nguyên và c là 1 t p con g m các s nguyên. ố ể ồ ậ ầ ố

ữ ệ ể ồ ị : Ví d 2ụ : Ta đ nh nghĩa ki u d li u Date, bao g m 2 thông tin là (tháng, ngày) nh sauư

9 Biên so n: Nguy n Tr n Thi Văn ễ

ầ

ạ

Ch

ng V: Đ c t

v i ngôn ng Z

Đ c t

Hình th c

ươ

ặ ả ớ

ữ

Bài gi ng môn ả

ặ ả

ứ

ướ ế ị do đ mô t ể ả ồ các tháng, bao g m ể ữ ệ ự : nh sau Tr 12 giá tr h ng riêng l ị ằ c h t, ta có đ nh nghĩa 1 ki u d li u t ẻ ư

Sau đó ta đ nh nghĩa ki u Date : ể ị

V.3.7 Gi n đ đ

c s d ng trong các khai báo

ả ồ ượ ử ụ

ả ặ ả c s d ng trong M t gi n đ , sau khi đ ồ ộ b t kỳ 1 khai báo nào. K t qu là các bi n có trong gi n đ s có m t trong ặ ấ khai báo đó, cùng v i nh ng ràng bu c t ả ớ c đ nh nghĩa và đ t tên, có th đ ế ộ ươ ứ ể ượ ử ụ ồ ẽ ả ng ng đã quy đ nh trên gi n đ . ồ ị ượ ị ế ữ

ớ ầ ớ ồ ố ụ ố ả ộ ậ ả ả ồ ờ Xét ví d sau, v i gi n đ SchemaTwo, g n gi ng v i SchemaOne nh ng có ư ầ ử ủ c a thêm 1 s ràng bu c, t p c ph i khác r ng, đ ng th i a ph i là 1 ph n t ỗ c.

Khi đó t p h p ậ ợ :

(cid:204) Z và c có ch a ph n t ứ t c các t p con c ậ ấ ả ợ s 0. Ta có th ầ ử ố ng, không s d ng gi n đ nh ử ụ ườ ả ồ ể ư s bao g m t ồ ẽ bi u di n t p h p này theo cách thông th ễ ậ ể sau :

ử ụ ễ ố ượ ộ ng thu c ho c cũng có th bi u di n theo 1 cách khác, s d ng 1 đ i t ki u SchemaTwo ể ể : ặ ể

i gi n đ mô t ki u Date trên : Ví d 2ụ : Tr l ở ạ ả ồ ả ể ở

10 Biên so n: Nguy n Tr n Thi Văn ễ

ầ

ạ

Ch

ng V: Đ c t

v i ngôn ng Z

Đ c t

Hình th c

ươ

ặ ả ớ

ữ

Bài gi ng môn ả

ặ ả

ứ

N u ta có th đ nh nghĩa t p các tháng có 31 ngày nh sau : ể ị ư ế ậ

hay nói 1 cách khác, đó là t pậ :

V.3.8 Gi n đ đ

c s d ng trong các bi u th c l

ng t

ả ồ ượ ử ụ

ứ ượ

ể

ừ

ư ể ả ồ ộ . Ví d ng t Nh đã kh ng đ nh, m t gi n đ có th đ nên nó có th xu t hi n trong các bi u th c l ệ ẳ ị ể ấ ể ượ ử ụ ứ ượ ữ ệ c s d ng nh 1 ki u d li u ư ụ : ừ ể

hay

V t ị ừ

còn có th đ c phát bi u theo 1 cách khác nh sau : ể ượ ư ể

V.3.9 Gi n đ đ

c s d ng nh 1 v t

ả ồ ượ ử ụ

ị ừ

ư

Xét gi n đ SchemaThree nh sau : ư ả ồ

Ta có th phát bi u ể ể :

r ng b t kỳ s nguyên a và t p s c nào th a ràng bu c trong ậ ấ ộ ỏ ố đ di n t ố ể ễ ả ằ SchemaThree thì cũng th a ràng bu c trong SchemaTwo. ỏ ộ

ng đ ng v i phát bi u sau : Phát bi u trên t ể ươ ươ ể ớ

11 Biên so n: Nguy n Tr n Thi Văn ễ

ầ

ạ

Ch

ng V: Đ c t

v i ngôn ng Z

Đ c t

Hình th c

ươ

ặ ả ớ

ữ

Bài gi ng môn ả

ặ ả

ứ

ủ ả ấ ậ ồ ượ ượ c c l i. Nh v y, ta nh n th y toàn b ph n khai báo c a 2 gi n đ đã đ ầ b , ch có ph n ràng bu c là đ c gi ỏ ư ậ ỉ ộ ượ l ữ ạ ầ ộ

V.3.10 D ng chu n c a 1 gi n đ

ẩ ủ

ả ồ

ạ

ị ả ồ ả ủ ầ ố ồ ấ ị ả ậ ộ ả ử ụ ầ ồ ư ả ủ ễ ị ỏ c gi n l Khi đ nh nghĩa 1 gi n đ , ph n khai báo c a gi n đ b n thân nó đã ch a ứ ị ừ s n 1 s ràng bu c nh t đ nh. Chính vì v y, khi s d ng gi n đ nh 1 v t ẵ thì các ràng bu c này cũng d b "b quên", do ph n khai báo c a gi n đ đã ồ đ ượ ộ c (xem ph n trên). ả ượ ầ

ể ẫ ả i. M t gi n đ ộ ộ ớ ả ộ Vì v y, đ tránh gây nh m l n, ta nên chuy n gi n đ v m t d ng m i sao ậ ể ồ cho t t c các ràng bu c đ u n m ph n ràng bu c bên d ằ ở ấ ả theo d ng này đ c g i là gi n đ chu n, và thao tác chuy n toàn b ràng ồ ượ ạ bu c xu ng ph n d ồ ượ ọ ố ầ ẩ c g i là chu n hóa gi n đ . ồ ầ ộ ề ả ọ i c a gi n đ đ ả ồ ề ộ ạ ướ ể ả ầ ướ ủ ẩ ộ

: Ví dụ : Xét gi n đ sau ả ồ

ng đ ng v i gi n đ ạ ồ ươ ả ể ố ự ồ ớ ộ nhiên N đã có ràng bu c : Tho t nhìn, ta có th nghĩ gi n đ này t ươ ể SchemaTwo, tuy nhiên, ngay trên b n thân ki u s t r i. Do v y, ta chu n hóa nó l ồ ả ả i nh sau ư ạ ẩ ậ

trên : Ví d 2ụ : Xét gi n đ Date ả ồ ở

Ta chu n hóa gi n đ này l : ẩ ả ồ ạ i nh sau ư

12 Biên so n: Nguy n Tr n Thi Văn ễ

ầ

ạ

Ch

ng V: Đ c t

v i ngôn ng Z

Đ c t

Hình th c

ươ

ặ ả ớ

ữ

Bài gi ng môn ả

ặ ả

ứ

V.3.11 Đ t l

i tên các thành ph n trong gi n đ

ặ ạ

ả ồ

ầ

ặ ả , đôi khi c n ph i đ t l ả ặ ạ ầ ả ể ạ ầ ế ấ ả Trong quá trình đ c t i tên các thành ph n trong 1 gi n đ . B ng cách này ta có th t o nên 1 gi n đ m i có cùng k t c u và ràng bu c v i gi n đ cũ nh ng có các thành ph n v i tên và ý nghĩa khác đi. ồ ằ ộ ớ ồ ớ ớ ư ầ ả ồ

Cú pháp đ đ i tên 1 gi n đ ể ổ ả ồ :

N u Schema là 1 gi n đ , ta ký hi u ệ : ế ả ồ

c t o nên b ng cách đ i tên thành ph n tên là old trong ả ồ ượ ạ ầ ằ ổ là gi n đ đ Schema thành new.

: Ví dụ : trong gi n đ SchemaTwo, n u thay a b ng q và c b ng s, ta có ế ằ ằ ả ồ

khi đó, gi n đ k t qu s t ng đ ng v i gi n đ ả ẽ ươ ồ ế ả ươ ả ớ ồ :

ng t nh v y, n u mu n đ nh nghĩa ki u d li u StartDate t ki u d ự ữ ệ ể ế ố ị ừ ể ữ : T ư ậ li u Date, ta có th làm nh sau ể ươ ệ ư

ng đ Khi đó, gi n đ s t ả ồ ẽ ươ ươ : ng

N u ta đ nh nghĩa thêm gi n đ FinishDate : ế ả ồ ị

ượ ư Khi đó, StartDate và FinishDate đ dù chúng đ u có 2 thành ph n và có các ràng bu c t c xem nh 2 ki u d li u khác nhau, m c ặ ể ữ ệ ng t nh nhau. ộ ươ ự ư ề ầ

V.4 Các phép toán trên gi n đả

ồ

V.4.1 Phép n i li n (Conjunction) ố ề

c th hi n nh sau, v i P và Q là 2 v t ả ị ừ ễ ả di n t ư ớ ể ệ ng ng: Cho 2 gi n đ S và T đ ượ ồ các ràng bu c lên các bi n t ế ươ ứ ộ

13 Biên so n: Nguy n Tr n Thi Văn ễ

ầ

ạ

Ch

ng V: Đ c t

v i ngôn ng Z

Đ c t

Hình th c

ươ

ặ ả ớ

ữ

Bài gi ng môn ả

ặ ả

ứ

Ta ký hi uệ : S (cid:217) T

ế c t o nên b ng cách g p các bi n trong S và T l ồ ả ẽ ự i, đ ng th i th c ồ ạ ố ề ủ ằ ả ờ ồ ế ộ đ bi u di n phép n i li n c a 2 gi n đ S và T. K t qu s là 1 gi n đ ể ể ả ễ m i đ ớ ượ ạ hi n phép n i li n trên 2 v t ố ề ệ ràng bu c P và Q. ộ ị ừ

ế ố ồ

c 2 gi n đ . N u không gi n đ S ả ố ầ ế ể ả ả ầ ả ồ L u ýư : N u trong 2 gi n đ S và T có 1 thành ph n gi ng nhau thì thành ồ (cid:217) T ph n này ph i có ki u gi ng nhau ở ả s không xác đ nh. ẽ ị

V.4.2 Phép đ i tên (Decoration)

ổ

s ta có gi n đ State mô t ả ầ 1 tr ng thái c a h th ng, có 2 thành ph n ủ ệ ố ạ Gi ồ a, b v i ràng bu c là P ả ử ớ ả ộ

M i đ i t ng s : State bi u di n 1 tr ng thái h p l c a h th ng. ỗ ố ượ ợ ệ ủ ệ ố ể ễ ạ

ạ ầ ử ụ ạ ể ể ạ ự ệ ệ ạ

ự ạ ể ạ ặ ả ấ ả ư ả ấ ồ c khai báo trong gi n đ : Đ bi u di n 1 thao tác lên 1 tr ng thái nào đó, ta c n s d ng 2 tr ng thái ễ c khi th c hi n thao tác và tr ng thái sau khi th c hi n thao tác tr ng thái tr ướ ồ đó. Đ phân bi t 2 tr ng thái này, ta dùng phép đ t tên đ t o nên 1 gi n đ ệ ể m i, b ng cách thêm d u nháy (’) vào sau tên gi n đ cũng nh tên t t c các ớ ằ ồ : bi n đ ế ượ ả

ể ư ả ầ Đ đ c t báo c a gi n đ . M t gi n đ thao tác s có d ng ả thao tác, ta có th đ a c 2 tr ng thái State và State’ vào ph n khai ả ể ặ ả ủ ạ : ạ ẽ ồ ộ ồ

14 Biên so n: Nguy n Tr n Thi Văn ễ

ầ

ạ

Ch

ng V: Đ c t

v i ngôn ng Z

Đ c t

Hình th c

ươ

ặ ả ớ

ữ

Bài gi ng môn ả

ặ ả

ứ

ễ ả ữ ứ ể ả ồ ị : Ngôn ng Z quy đ nh 1 cách th c bi u di n c 2 gi n đ State và State’, cách th c bi u di n đó nh sau ễ ư ứ ể

V.4.3 Phép n i r i (Disjunction) ố ờ

c th hi n nh sau, v i P và Q là 2 v t ả ị ừ ễ ả di n t ư ớ ể ệ ng ng: Cho 2 gi n đ S và T đ ượ ồ các ràng bu c lên các bi n t ế ươ ứ ộ

Ta ký hi uệ : S (cid:218) T

ễ ế ả ả c t o nên b ng cách g p các bi n trong S và T l ố ờ ủ ộ ự ế ạ ằ đ bi u di n phép n i r i c a 2 gi n đ S và T. K t qu s là 1 gi n đ m i ồ ớ ả ẽ ồ ể ể đ ệ i, đ ng th i th c hi n ờ ồ ượ ạ phép n i r i trên 2 v t ràng bu c P và Q. ộ ố ờ ị ừ

ng t ấ ả ế ấ

ầ ầ ề nh trên phép n i li n, t T ự ư ầ ố ề ươ c 2 gi n đ thành ph n ph i có cùng ki u d li u. ả ở ả ả ồ n u có xu t hi n ệ ở ấ ế ràng bu c c a m i gi n đ thành ph n tr ỗ ộ ủ ệ t c các thành ph n (các bi n) xu t hi n ữ ệ T t c các ràng bu c ộ c chuy n sang ph n v t ị ừ ự ấ ả ể ể ả ượ c khi th c hi n phép n i r i. ệ ph n khai báo đ u ph i đ ả ầ ố ờ ướ ầ ồ

V.4.4 Phép ph đ nh (Negation) ủ ị

c th hi n nh sau, v i P là v t ể ệ di n t ị ừ ễ ả ư ớ ộ các ràng bu c Cho gi n đ S T đ ồ ả lên các bi n t ượ ng ng: ế ươ ứ

15 Biên so n: Nguy n Tr n Thi Văn ễ

ầ

ạ

Ch

ng V: Đ c t

v i ngôn ng Z

Đ c t

Hình th c

ươ

ặ ả ớ

ữ

Bài gi ng môn ả

ặ ả

ứ

khi đó gi n đ ph đ nh ồ ủ ị ả (cid:216) S s có d ng ạ : ẽ

ượ ụ ả ồ ỉ ứ c chuy n sang ph n v t ả ượ ể ề c chu n hóa (t c là ẩ ràng bu c bên ị ừ ộ L u ýư : phép ph đ nh ch áp d ng cho các gi n đ đã đ ủ ị t t c các ràng bu c đ u ph i đ ầ ộ ấ ả i).ướ d

ữ ễ (cid:216) Date sẽ t c nh ng c p (month, day) nào không ph i là m t ngày tháng , do đó ộ ể ặ ữ

Ví dụ : Gi n đ Date bi u di n nh ng ngày tháng h p l ả ợ ệ ồ bi u di n t ả ễ ấ ả ể h p l . ợ ệ

V.4.5 Phép l

ng t

hóa

ượ

ừ

ể ạ ố ả ả và dec là ph n khai báo, khi đó gi n đ đ ồ đ t o ra 1 gi n đ ả ầ ủ ầ ồ ồ ượ c ừ hóa s có d ng hóa 1 s thành ph n c a 1 gi n đ ng t Ta có th l ể ượ ừ m i. N u ế Q là 1 l ượ ớ ng t l ừ ượ ng t ạ : ẽ

ằ ả ầ Q trong ph n v t ỏ hóa chúng b ng l ng t ầ c t o thành b ng cách b đi các thành ph n có trong ph n ượ ạ ràng ng t ượ ị ừ ượ ừ ừ ầ ằ Gi n đ này đ ồ khai báo dec và l bu c bên d i. ướ ộ

•

: Ví dụ : cho gi n đ nh sau ả ồ ư

SBb

" Khi đó, là gi n đả ồ :

16 Biên so n: Nguy n Tr n Thi Văn ễ

ầ

ạ

Ch

ng V: Đ c t

v i ngôn ng Z

Đ c t

Hình th c

ươ

ặ ả ớ

ữ

Bài gi ng môn ả

ặ ả

ứ

•

SBb

$ và là gi n đả ồ :