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

 ðc t  Z (5)
 Nguy n Thanh Bình
 Khoa Công ngh Thôngtin
 Tr ưng ði h c Bách khoa
 ði h c ðà Nng
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  dng r ng rãi 
 nh t

 da trên lý thuy t t p h p

 ký hi u toán h c

 s dng các s ơ ñ (schema)
  d hi u
2
 1
Gi i thi u

 Gm bn thành ph n cơ b n
  các ki u d  li u (types)
 • da 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 ơ ñ mi t  các s ơ ññãc ó
3
Kiu d  li u

 mi ki u d  li u là mt tp 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
Kiu d  li u

 Các phép toán trên t p h p
  Hi: A ∪ B 
  Giao: A ∩ B
  Hi u: A ⁄ B
  Tp con: A ⊆ B
  Tp các t p con: P A
 • ví d: P {a, b} = {{}, {a}, {b}, {a, b}}
5
Kiu d  li u

 mt 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 dng c p ký hi u [ và]ññnh ngh ĩa ki u c ơ 
 bn m i
6
 3
Kiu d  li u

 Khai báo ki u
  x : T
 • x là ph n t  ca t p T
  Ví d
 • x : R
 • n : N
 • 3 : N
 • red : {red, blue, green}
7
V t

 Mt v  t( predicate) ñưc s  dng ññ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 dng các toán t  lô-gíc ññnh ngh ĩa các v 
 t ph c t p
  Và: A ∧ B
  Ho c: A ∨ B
  Ph ñnh: ¬ A
  Kéo theo: 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 mi x thu c T
 • Ví d: ( ∀x : N • x - x =0)
  (∃x : T • A)
 • A ñúng v i mt 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

 Cu 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
 • ñiu 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  mi 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
 • tp h p các ng ưi s  dng h  th ng user
 • tp h p các nhân viên ñang vào in
 • tp h p các nhân viên ñang ra out
 bt 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  ca 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 
 ca h  th ng
  Bt bi n: ràng bu c gi a các ñi t ưng
  Các s ơ ñ thao tác
 • ðiu ki n trên các tham s  vào
 • Quan h  gi a tr ng thái tr ưc và sau
 • Tham s  kt 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 ñ to ra 
 các s ơ ñ mi

 Các toán t sơñ
  Và: ∧
  Ho c: ∨
23
Toán t sơñ

 Các s ơ ññãc ó

 To các s ơ ñ mi
  Schema3 == Schema1 ∧ Schema2
  Schema4 == Schema1 ∨ Schema2
24
 12
Ví d 1 (ti p)

 Ci ti n thao tác StaffQuery
  Thao tác StaffQuery chưañc t trưng h p 
 li
 • name? ∉ users
25
Ví d 1 (ti p)

 Ci ti n thao tác StaffQuery
  ðc t  li ki u QueryReply 
 QueryReply == is_in | is_out | not_registered

 Khi ñó
 RobustStaffQuery == StaffQuery ∨ BadStaffQuery
26
 13
Ví d 1 (ti p)

 Ci ti n thao tác CheckIn
 
 M rng thao tác cho tr ưng h p ghi nh n thành công
27
Ví d 1 (ti p)

 Ci ti n thao tác CheckIn
  M rng 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)

 Ci ti n thao tác CheckIn
  Xlýthêmhaitrưng h p l i
 1. name? ñãñưc ghi nh n
 2. name? chưa ñưc ñă ng ký
29
Ví d 1 (ti p)

 Ci ti n thao tác CheckIn
  Xlýthêmhaitrưng h p l i
30
 15
Ví d 1 (ti p)

 Ci ti n thao tác CheckIn
  Khi ñó
 CheckInReply == ok | already_in | not_registered
 RobustCheckIn == GoodCheckIn 
 ∨ BadCheckIn1 
 ∨ BadCheckIn2
31
Quan h 

 Cp ph n t  có th  tñưc bi u 
 di n
  (x, y)

 Tích ð-các ca hai ki u T1 và T2
  T1 x T2
  (x, y) : T1 x T2
32
 16
Quan h 

 Quan h  (relation) là tp 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 
  cp ph n t  có th  t (x, y) có th  vi t
 • Ví d

 Lưu ý
  kí hi u ↔ dành cho ki u
  kí hi u dành cho giá tr 
34
 17
Quan h 

 Domain và Range
  tp 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}
  tp 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 ñin tho i g m tên ng ưi và
 sñin tho i
  S dng 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 ñin tho i
39
Ví d 2
 có th  ci ti n ?

 Tìm s ñin tho i c a m t ng ưi

 Tìm tên theo s ñin tho i
40
 20
Ví d 2

 Xóa s ñin tho i c a m t ng ưi
41
Ví d 2

 Xóa các m c trong danh b  ng v i m t tên

 Xóa các m c trong danh b  ng v i m t t p các 
 tên
42
 21
Partial Function

 là quan h  mà mi ph n t  trong domain cho m t 
 giá tr  duy nh t trong range

 ký hi u

 ngh ĩa là
43
Partial Function

 Ví d

 Có th  áp d ng các toán t  hàm
44
 22
Partial Function

 Toán t  quá tải hàm (Function Overriding)
  thay th  mt m c vào b i m t m c m i
  ký hi u
  ví d
  lưu ý
45
Ví d 3

 ðc t  h th ng qu n lý ngày sinh
  s dng ki u c ơ b n m i
 [Person, Date]
  mi ng ưi ch  có mt ngày sinh duy nh t
  kh i t o h  th ng
46
 23
Ví d 3

 Thêm m t ng ưi vào h  th ng
47
Ví d 3
 ðiu gì xy ra n u name? ∉∉∉ dom(bb)

 Ch nh s a ngày sinh

 Xóa m t ng ưi
48
 24
Ví d 3

 Tìm ngày sinh c a m t ng ưi
49
Ví d 3

 Tìm ngày sinh c a m t ng ưi
  tr ưng h p tìm không th y
50
 25
Ví d 3

 Tìm ngày sinh c a m t ng ưi
  thông báo khi tìm th y
  khi ñó
51
Ví d 3

 Tìm nh ng ng ưi cùng ngày sinh
52
 26
Total Function

 ñnh ngh ĩa ánh x  t tt c  giá tr  ca domain ñn 
 range

 ký hi u

 ngh ĩa là
53
Total Function

 Ví d
54
 27
 Total Function
 
 S dng ññnh ngh ĩa h ng s 
 
 Ví d
 55
 Các ký hi u
Toán t  lô-gíc Tp h p Quan h  và Hàm
 56
 28