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
2
3
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


 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
4
7
Kiểu dữ liệu


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
∈


ñị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ừ
7
13
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

ðặ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ơ ñồ ñã 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


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ệ

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ệ

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

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