Bài giảng Công nghệ phần mềm - Chương 5.2: Đặc tả Z - Nguyễn Thanh Bình
Bạn đang xem 20 trang mẫu của tài liệu "Bài giảng Công nghệ phần mềm - Chương 5.2: Đặc tả Z - Nguyễn Thanh Bình", để tải tài liệu gốc về máy bạn click vào nút DOWNLOAD ở trên
Tài liệu đính kèm:
bai_giang_cong_nghe_phan_mem_chuong_5_2_dac_ta_z_nguyen_than.pdf
Nội dung text: Bài giảng Công nghệ phần mềm - Chương 5.2: Đặ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