Giáo Trình Công Nghệ Phần Mềm part 3

Tham khảo tài liệu 'giáo trình công nghệ phần mềm part 3', công nghệ thông tin, kỹ thuật lập trình phục vụ nhu cầu học tập, nghiên cứu và làm việc hiệu quả
Nội dung trích xuất từ tài liệu:
Giáo Trình Công Nghệ Phần Mềm part 3 ð 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 ð ih 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: A∩B Hi u: 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 nm 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à: 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 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 t ...