Đặc tả Z5

1ðặ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 2 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ử 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 23 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ó 4 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} 35 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}} 6 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ản mới 47 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} 8 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  pi ∈ R 59 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) 10 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} 611 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ừ 12 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ừ 713 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 14 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ự “!” 815 Sơ ñồ thao tác
Kí hiệu Ξ mô tả thao tác không thể thay ñổi biến trạng thái 16 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 917 Ví dụ 1
ðặc tả thao tác ghi nhận một nhân viên vào 18 Ví dụ 1
ðặc tả thao tác ghi nhận một nhân viên ra 10 19 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 20 Ví dụ 1
Khởi tạo hệ thống 11 21 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 22 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 12 23 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: ∨ 24 Toán tử sơ ñồ
Các sơ ñồ ñã có
Tạo các sơ ñồ mới  Schema3 == Schema1 ∧ Schema2  Schema4 == Schema1 ∨ Schema2 13 25 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 26 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 14 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 28 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 15 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 1. name? ñã ñược ghi nhận 2. name? chưa ñược ñăng ký 30 Ví dụ 1 (tiếp)
Cải tiến thao tác CheckIn  Xử lý thêm hai trường hợp lỗi 16 31 Ví dụ 1 (tiếp)
Cải tiến thao tác CheckIn  Khi ñó CheckInReply == ok | already_in | not_registered RobustCheckIn == GoodCheckIn ∨ BadCheckIn1 ∨ BadCheckIn2 32 Quan hệ
Cặp phần tử có thứ tự ñược biểu diễn  (x, y)
Tích ðề-các của hai kiểu T1 và T2  T1 x T2  (x, y) : T1 x T2 17 33 Quan hệ
Quan hệ (relation) là tập các cặp phần tử có thứ tự  Ví dụ: 34 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ị 18 35 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} 36 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à: 19 37 Quan hệ
Phép trừ miền (domain subtraction)  Ví dụ:  Khi ñó: 38 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 20 39 Ví dụ 2
Khởi tạo hệ thống
Thêm một số ñiện thoại 40 Ví dụ 2
Tìm số ñiện thoại của một người
Tìm tên theo số ñiện thoại có thể cải tiến ? 21 41 Ví dụ 2
Xóa số ñiện thoại của một người 42 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 22 43 Partial Function
là quan hệ mà mỗi phần tử trong domain cho một giá trị duy nhất trong range
ký hiệu
nghĩa là 44 Partial Function
Ví dụ
Có thể áp dụng các toán tử hàm 23 45 Partial Function
Toán tử quá tải hàm (Function Overriding)  thay thế một mục vào bởi một mục mới  ký hiệu  ví dụ  lưu ý 46 Ví dụ 3
ðặc tả hệ thống quản lý ngày sinh  sử dụng kiểu cơ bản mới [Person, Date]  mỗi người chỉ có một ngày sinh duy nhất  khởi tạo hệ thống 24 47 Ví dụ 3
Thêm một người vào hệ thống 48 Ví dụ 3
Chỉnh sửa ngày sinh
Xóa một người ðiều gì xảy ra nếu name? ∉ dom(bb) 25 49 Ví dụ 3
Tìm ngày sinh của một người 50 Ví dụ 3
Tìm ngày sinh của một người  trường hợp tìm không thấy 26 51 Ví dụ 3
Tìm ngày sinh của một người  thông báo khi tìm thấy  khi ñó 52 Ví dụ 3
Tìm những người cùng ngày sinh 27 53 Total Function
ñịnh nghĩa ánh xạ từ tất cả giá trị của domain ñến range
ký hiệu
nghĩa là 54 Total Function
Ví dụ 28 55 Total Function
Sử dụng ñể ñịnh nghĩa hằng số
Ví dụ 56 Các ký hiệu Toán tử lô-gíc Tập hợp Quan hệ và Hàm