Đặc tả Z

Chia sẻ: Võ Quang Hòa | Ngày: | Loại File: PDF | Số trang:28

Thêm vào BST

Báo xấu

227
lượt xem 67
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Ngôn ngữ Z không được thiết kế để mô tả các yêu cầu phi chức năng của hệ thống, ví dụ như công dụng, hiệu năng, kích thước hay độ tin cậy của hệ thống. Ngôn ngữ cũng không được thiết kế cho các đặc tả theo thời gian hay xử lý song song. Muốn làm được điều này, ta phải kết hợp Z cùng với các công cụ khác nữa.

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: Đặ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 ð 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 A∪B H i: A∩B Giao: A⁄B Hi u: A⊆B T p con: 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 k i u d l i u c ơ b n ñ ã ñư c ñ n h nghĩa trư c ki u s nguyên Z ki u s t nhiên N ki u s t h 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 Vt 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
Vt Có th s d ng các toán t lô-gíc ñ ñ nh nghĩa các v t ph c t p A∧B Và: A∨B Ho c : ¬A Ph ñ nh: 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 Vt 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 li • 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 bi u C p ph n t có th t 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 kí hi 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