Bài giảng Công nghệ phần mềm - Chương 5: Đặc tả Z

ðꢀc tꢁ Z (5)

Nguyꢀn Thanh Bình

Khoa Công nghꢁꢂThôngꢂtin

Trưꢃng ðꢄi hꢅc Bách khoa

ðꢄi hꢅc ðà Nꢆng

Giꢂi thiꢃu

ꢀ

ñưꢄc ñꢅ xuꢆt bꢇi Jean René Abrial ꢇꢈðꢉi hꢊc

Oxford

ꢀ

ngôn ngꢋꢈñꢀc tꢁ hình thꢌc ñưꢄc sꢍ dꢎng rꢏng rãi

nhꢆt

ꢀ

dꢐa trên lý thuyꢑt tꢒp hꢄp

ký hiꢃu toán hꢊc

sꢍ dꢎng các sơ ñꢓ (schema)

ꢁ

dꢔ hiꢕu

2

1

Giꢂi thiꢃu

ꢀ

Gꢓm bꢖn thành phꢗn cơ bꢁn

ꢁ

các kiꢕu dꢋ liꢃu (types)

• dꢐa trên khái niꢃm tꢒp hꢄp

các sơ ñꢓ trꢉng thái (state schemas)

• mô tꢁ các biꢑn và ràng buꢏc trên các biꢑn

các sơ ñꢓ thao tác (operation schemas)

• mô tꢁ các thao tác (thay ñꢘi trꢉng thái)

các toán tꢍꢈsơꢈñꢓ (schema operations)

• ñꢙnh nghĩa các sơ ñꢓ mꢂi tꢚ các sơ ñꢓꢈñãꢈcó

3

Kiꢕu dꢋ liꢃu

ꢀ

mꢛi kiꢕu dꢋ liꢃu là mꢏt tꢇp hꢈp các phꢗn tꢍ

ꢀ

Ví dꢎ

ꢁ

{true, false} : kiꢕu lô-gíc

N: kiꢕu sꢖ tꢐ nhiên

Z: kiꢕu sꢖ nguyên

R: kiꢕu sꢖ thꢐc

{red, blue, green}

4

2

Kiꢕu dꢋ liꢃu

ꢀ

Các phép toán trên tꢒp hꢄp

ꢁ

Hꢏi:

A

B

Giao:

Hiꢃu:

A ∩ B

A ⁄ B

Tꢒp con:

A B

Tꢒp các tꢒp con: P A

• ví dꢎ: P {a, b} = {{}, {a}, {b}, {a, b}}

5

Kiꢕu dꢋ liꢃu

ꢀ

mꢏt sꢖ kiꢕu dꢋ liꢃu cơ bꢁn ñã ñưꢄc ñꢙnh

nghĩa trưꢂc

ꢁ

kiꢕu sꢖ nguyên Z

kiꢕu sꢖ tꢐ nhiên N

kiꢕu sꢖ thꢐc R

...

ꢀ

có thꢕꢈñꢙnh nghĩa các kiꢕu dꢋ liꢃu mꢂi

ꢁ

ANSWER == yes | no

ꢁ

[PERSON]

• sꢍ dꢎng cꢀp ký hiꢃu [ vàꢈ]ꢈñꢕꢈñꢙnh nghĩa kiꢕu cơ

bꢁn mꢂi

6

3

Kiꢕu dꢋ liꢃu

ꢀ

Khai báo kiꢕu

ꢁ

x : T

• x là phꢗn tꢍ cꢜa tꢒp T

ꢁ

Ví dꢎ

• x : R

• n : N

• 3 : N

• red : {red, blue, green}

7

Vꢙ tꢚ

ꢀ

Mꢏt vꢙ tꢚꢈ(predicate)ꢈñưꢄc sꢍ dꢎng ñꢕꢈñꢙnh

nghĩa các tính chꢆt cꢜa biꢑn/giá trꢙ

ꢀ

Ví dꢎ

ꢁ

x > 0

π

R

8

4

Vꢙ tꢚ

ꢀ

Có thꢕ sꢍ dꢎng các toán tꢍ lô-gíc ñꢕꢈñꢙnh nghĩa các vꢙ

tꢚ phꢌc tꢉp

ꢁ

Và:

Hoꢀc:

Phꢜꢈñꢙnh:

Kéo theo:

A

¬

B

A

⇒ B

ꢀ

Ví dꢎ

ꢁ

(x > y) (y > 0)

(x > 10) (x = 1)

(x > 0) ) x/x = 1

(x S)) (x T)

⇒

(

¬

9

Vꢙ tꢚ

ꢀ

Các toán tꢍ khác

ꢁ

( x : T • A)

• A ñúng vꢂi mꢅi x thuꢏc T

• Ví dꢎ: ( x : N • x - x =0)

( x : T • A)

• A ñúng vꢂi mꢉt sꢊ giá trꢙ x thuꢏc T

• Ví dꢎ: ( x : R • x + x = 4)

{x : T | A}

• biꢕu diꢔn các phꢗn tꢍ x cꢜa T thꢝa mãn A

• Ví dꢎ: N = {x : Z | x ≥ 0}

10

5

Sơ ñꢓ trꢉng thái

ꢀ

Cꢆu trúc sơ ñꢓ trꢉng thái gꢓm

ꢁ

tên sơ ñꢓ

khai báo biꢑn

ñꢙnh nghĩa vꢙ tꢚ

11

Sơ ñꢓ trꢉng thái

ꢀ

ðꢀc tꢁ Z chꢌa

ꢁ

các biꢑn trꢉng thái

khꢇi gán biꢑn

các thao tác trên các biꢑn

ꢁ

biꢑn trꢉng thái có thꢕ có các bꢆt biꢑn

• ñiꢅu kiꢃn màꢈluônꢈñúng, biꢕu diꢔn bꢇi các vꢙ tꢚ

12

6

Sơ ñꢓ thao tác

ꢀ

Khꢇi gán biꢑn

ꢀ

Khai báo thao tác trên biꢑn

ꢁ

kí hiꢃu ∆ biꢕu diꢔn biꢑn trꢉng thái bꢙꢈthayꢈñꢘi bꢇi thao

tác

ꢁ

kí hiꢃu ‘ (dꢆu nháy ñơn) biꢕu diꢔn giá trꢙ mꢂi cꢜa biꢑn

13

Sơ ñꢓ thao tác

ꢀ

Thao tác có thꢕ có các tham sꢖ vào và ra

ꢁ

tên tham sꢖ vào kꢑt thúc bꢇi kí tꢐ “?”

tên tham sꢖ ra kꢑt thúc bꢇi kí tꢐ “!”

14

7

Sơ ñꢓ thao tác

ꢀ

Kí hiꢃu Ξ mô tꢁ thao tác không thꢕꢈthayꢈñꢘi

biꢑn trꢉng thái

15

Ví dꢎ 1

ꢀ

ðꢀc tꢁ hꢃ thꢖng ghi nhꢒn các nhân viên vào/ra tòa

nhà làm viꢃc

ꢁ

Kiꢕu dꢋ liꢃu [Staff] là kiꢕu cơ bꢁn mꢂi cꢜa hꢃ thꢖng

ꢁ

Trꢉng thái cꢜa hꢃ thꢖng bao gꢓm

• tꢒp hꢄp các ngưꢞi sꢍ dꢎng hꢃ thꢖng user

• tꢒp hꢄp các nhân viên ñang vào in

• tꢒp hꢄp các nhân viên ñang ra out

bꢆt biꢑn cꢜa hꢃ thꢖng

16

8

Ví dꢎ 1

ꢀ

ðꢀc tꢁ thao tác ghi nhꢒn mꢏt nhân viên vào

17

Ví dꢎ 1

ꢀ

ðꢀc tꢁ thao tác ghi nhꢒn mꢏt nhân viên ra

18

9

Ví dꢎ 1

ꢀ

ðꢀc tꢁ thao tác kiꢕm tra mꢏt nhân viên vào hay ra

ꢁ

Thao tác này cho kꢑt quꢁ là phꢗn tꢍ cꢜa kiꢕu

QueryReply == is_in | is_out

ðꢀc tꢁ thao tác

ꢁ

19

Ví dꢎ 1

ꢀ

Khꢇi tꢉo hꢃ thꢖng

20

10

Ví dꢎ 1

ꢀ

Tóm lꢉi

ꢁ

Sơ ñꢋ trꢄng thái: các thành phꢗn/ñꢖi tưꢄng

cꢜa hꢃ thꢖng

ꢁ

Bꢌt biꢍn: ràng buꢏc giꢋa các ñꢖi tưꢄng

Các sơ ñꢋ thao tác

• ðiꢅu kiꢃn trên các tham sꢖ vào

• Quan hꢃ giꢋa trꢉng thái trưꢂc và sau

• Tham sꢖ kꢑt quꢁ

ꢁ

Khꢎi gán

21

Ví dꢎ 1

ꢀ

Hãy ñꢀc tꢁ các thao tác

ꢁ

Register: thêm vào mꢏt nhân viên mꢂi

ꢁ

QueryIn: cho biꢑt nhꢋng nhân viên ñang

vào/làm viꢃc

22

11

Toán tꢍꢈsơꢈñꢓ

ꢀ

Các sơ ñꢓ có thꢕꢈñưꢄc kꢑt hꢄp ñꢕ tꢉo ra

các sơ ñꢓ mꢂi

ꢀ

Các toán tꢍꢈsơꢈñꢓ

ꢁ

Và:

ꢁ

Hoꢀc:

23

Toán tꢍꢈsơꢈñꢓ

ꢀ

Các sơ ñꢓꢈñãꢈcó

ꢀ

Tꢉo các sơ ñꢓ mꢂi

ꢁ

Schema3 == Schema1 Schema2

Schema4 == Schema1 Schema2

ꢁ

24

12

Ví dꢎ 1 (tiꢑp)

ꢀ

Cꢁi tiꢑn thao tác StaffQuery

ꢁ

Thao tác StaffQueryꢈchưaꢈñꢀc tꢁꢈtrưꢞng hꢄp

lꢛi

• name? users

25

Ví dꢎ 1 (tiꢑp)

ꢀ

Cꢁi tiꢑn thao tác StaffQuery

ꢁ

ðꢀc tꢁ lꢉi kiꢕu QueryReply

QueryReply == is_in | is_out | not_registered

ꢀ

Khi ñó

RobustStaffQuery == StaffQuery BadStaffQuery

26

13

Ví dꢎ 1 (tiꢑp)

ꢀ

Cꢁi tiꢑn thao tác CheckIn

ꢀ

Mꢇ rꢏng thao tác cho trưꢞng hꢄp ghi nhꢒn thành công

27

Ví dꢎ 1 (tiꢑp)

ꢀ

Cꢁi tiꢑn thao tác CheckIn

ꢁ

Mꢇ rꢏng thao tác cho trưꢞng hꢄp ghi nhꢒn thành

công

ꢀ

Khi ñó

GoodCheckIn == CheckIn Success

28

14

Ví dꢎ 1 (tiꢑp)

ꢀ

Cꢁi tiꢑn thao tác CheckIn

ꢁ

Xꢍꢈlýꢈthêmꢈhaiꢈtrưꢞng hꢄp lꢛi

1. name?ꢈñãꢈñưꢄc ghi nhꢒn

2. name? chưa ñưꢄc ñăng ký

29

Ví dꢎ 1 (tiꢑp)

ꢀ

Cꢁi tiꢑn thao tác CheckIn

Xꢍꢈlýꢈthêmꢈhaiꢈtrưꢞng hꢄp lꢛi

ꢁ

30

15

Ví dꢎ 1 (tiꢑp)

ꢀ

Cꢁi tiꢑn thao tác CheckIn

ꢁ

Khi ñó

CheckInReply == ok | already_in | not_registered

RobustCheckIn == GoodCheckIn

BadCheckIn1

BadCheckIn2

31

Quan hꢃ

ꢀ

Cꢏp phꢐn tꢑ có thꢒ tꢓꢈñưꢄc biꢕu

diꢔn

ꢁ

(x, y)

ꢀ

Tích ðꢔ-các cꢜa hai kiꢕu T1 và T2

ꢁ

T1 x T2

(x, y) : T1 x T2

32

16

Quan hꢃ

ꢀ

Quan hꢁ (relation) là tꢒp các cꢀp

phꢗn tꢍ có thꢌ tꢐ

ꢁ

Ví dꢎ:

33

Quan hꢃ

ꢀ

Có thꢕ ký hiꢃu quan hꢃ

ꢁ

T

↔

S == P (T x S)

ꢁ

directory : Person

↔

Number

ꢀ

Ánh xꢉ

cꢀp phꢗn tꢍ có thꢌ tꢐ (x, y) có thꢕ viꢑt

ꢁ

•

Ví dꢎ

ꢀ

Lưu ý

ꢁ

kí hiꢃu

↔

dành cho kiꢕu

dành cho giá trꢙ

ꢁ

34

17

Quan hꢃ

ꢀ

Domain và Range

ꢁ

tꢒp hꢄp các thành phꢗn thꢌ nhꢆt trong mꢏt quan hꢃꢈ

ñưꢄc gꢊi là domain (miꢅn)

• kí hiꢃu: dom

• ví dꢎ:

dom(directory) = {mary, john, jim, jane}

ꢁ

tꢒp hꢄp các thành phꢗn thꢌ hai trong mꢏt quan hꢃꢈ

ñưꢄc gꢊi là range

• kí hiꢃu: ran

• ví dꢎ:

ran(directory) = {287373, 398620, 829483, 493028}

35

Quan hꢃ

ꢀ

Phép trꢚ miꢅn (domain subtraction)

ꢁ

ký hiꢃu:

ꢁ

biꢕu diꢔn quan hꢃ R vꢂi các phꢗn tꢍ

trong miꢅn S ñã bꢙ loꢉi bꢝ

Nghĩa là:

ꢁ

36

18

Quan hꢃ

ꢀ

Phép trꢚ miꢅn (domain subtraction)

ꢁ

Ví dꢎ:

ꢁ

Khi ñó:

37

Ví dꢎ 2

ꢀ

ðꢀc tꢁ danh bꢉꢈñiꢃn thoꢉi gꢓm tên ngưꢞi và

sꢖꢈñiꢃn thoꢉi

ꢁ

Sꢍ dꢎng kiꢕu cơ bꢁn

[Person, Phone]

ꢁ

ðꢀc tꢁ trꢉng thái hꢃ thꢖng

38

19

Ví dꢎ 2

ꢀ

Khꢇi tꢉo hꢃ thꢖng

ꢀ

Thêm mꢏt sꢖꢈñiꢃn thoꢉi

39

Ví dꢎ 2

có thꢕ cꢁi tiꢑn ?

ꢀ

Tìm sꢖꢈñiꢃn thoꢉi cꢜa mꢏt ngưꢞi

ꢀ

Tìm tên theo sꢖꢈñiꢃn thoꢉi

40

20

Bài giảng Công nghệ phần mềm - Chương 5: Đặc tả Z - Nguyễn Thanh Bình