Công nghệ phần mềm - Ðặc tả Z

Nội dung text: Công nghệ phần mềm - Ðặc tả Z

1. ð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
2. 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
3. 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
4. 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
5. 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
6. 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
7. 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
8. 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
9. 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
10. 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
11. 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
12. 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
13. 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
14. 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
15. 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
16. 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
17. 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
18. 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
19. 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
20. 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
21. 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
22. 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
23. 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
24. 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
25. 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
26. 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
27. 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
28. 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