Công nghệ phần mềm - Đặ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