Bài giảng Ðặc tả Z

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