03.KieuTapHop Dac Ta Hinh Thuc

1
Chương 3 Mô hình hóa dữ liệu
Kiểu tập hợp
Giảng viên: PGS.TS. Vũ Thanh Nguyên
Trường Đại học Công Nghệ Thông Tin, ĐHQG-HCM
Khoa Công Nghệ Phần Mềm
2
Kiểu dữ liệu trong VDM
Các kiểu dữ liệu đơn giản được định nghĩa sẵn:
ℕ, ℕ1, ℤ, ℝ, ℚ, B, Char
3
Các tập hợp được định nghĩa sẵn
Tập số nguyên ℤ = {…, -2, -1, 0, 1, 2, …}
Tập số tự nhiên ℕ = {0, 1, 2, 3, …}
Tập số nguyên dương ℕ1 = {1, 2, 3, …}
Tập số thực ℝ
Tập số hữu tỉ ℚ
Tập boolean B = {true, false}
Tập ký tự (gồm chữ cái hoa/thường, số, phép toán, dấu câu)
Char = {‘a’, ‘b’, ‘c’, ‘d’, ‘e’, ‘f’, ‘g’, ‘h’, ‘i’, ‘j’, ‘k’, ‘l’, ‘m’,
‘n’, ‘o’, ‘p’, ‘q’, ‘r’, ‘s’, ‘t’, ‘u’, ‘v’, ‘w’, ‘x’, ‘y’, ‘z’,
‘A’, ‘B’, ‘C’, ‘D’, ‘E’, ‘F’, ‘G’, ‘H’, ‘I’, ‘J’, ‘K’, ‘L’, ‘M’,
‘N’, ‘O’, ‘P’, ‘Q’, ‘R’, ‘S’, ‘T’, ‘U’, ‘V’, ‘W’, ‘X’, ‘Y’, ‘Z’,
‘0’, ‘1’, ‘2’, ‘3’, ‘4’, ‘5’, ‘6’, ‘7’, ‘8’, ‘9’, ‘+’, ‘-’, ‘=‘, ‘<‘, ‘>’,
‘*’, ‘/’, ‘(‘, ‘)’, ‘[‘, ‘]’, ‘{‘, ‘}’, ‘.’, ‘,’, ‘?’, ‘!’, …}
4
Mô hình hóa dữ liệu
Technical-Staff =
{PROJECT-MANAGER, TEAM-LEADER, ANALYST, DESIGNER, PROGRAMMER, TESTER}
5
Kiểu tập hợp
Cho trước kiểu dữ liệu T
Cần định nghĩa kiểu dữ liệu, trong đó, mỗi thể hiện là 1 tập hợp các phần tử thuộc kiểu dữ liệu T
Ký hiệu: T-set

Ví dụ 1:
Mode = {READ, WRITE, EXECUTE}
FileMode = Mode-set
FileMode = { {}, {READ}, {WRITE}, {EXECUTE}, {READ, WRITE}, {READ, EXECUTE}, {EXECUTE, WRITE}, {READ, WRITE, EXECUTE} }
Ví dụ 2:
Intset = ℤ-set
6
Kiểu tập hợp
Ví dụ 3:
Pupils = { Patrick, Christa, Emma, Pete, Frank, Lisa, Richard, David, Daniel, John, Helen, Pauline, Mark, Mike, Elisabeth}
School-trip = Pupils-set
7
Kiểu tập hợp
Câu hỏi: Có thể sử dụng kiểu tập hợp cho các trường hợp nào sau đây:
Hành khách trên 1 chuyến xe buýt
Bệnh nhân trong phòng chờ khám bệnh trong 1 buổi
Thí sinh được nhận giải thưởng trong 1 kỳ thi
8
Mô hình hóa các operation
Một operation có thể có hai tác dụng
Thay đổi nội dung biến bên ngoài
Trả về giá trị thông qua tham số kết quả
Đối với các biến bên ngoài:
Biến được truy xuất dạng read-only (rd)
Biến được truy xuất dạng read-write (wr)
Không có dạng truy xuất write-only trong VDM

Ví dụ:
ext rd size: ℕ
ext wr a, b: ℕ, rd x: ℤ
9
Đặc tả operation
Tên_Operation (thamsố1: Kiểu1, thamsố2: Kiểu2…) kq: Kiểukq
ext wr BiếnRead_Write: Kiểu,
rd BiếnRead_Only: Kiểu
pre Vị từ pre-condition
post Vị từ post-condition
10
Đặc tả operation
Ví dụ

MULT (heso: ℝ)
ext wr x: ℝ
pre x < 16384
post x = heso  x

ADD-TO-TRIP (new-on-trip: School-trip)
ext wr trip: School-trip
pre  new-on-trip  trip
post trip = trip  new-on-trip
⃐
↼
11
Đặc tả operation
Ví dụ
dấu có nghĩa là post (post condition - điều kiện sau) chỉ đến giá trị của toán hạng (biến) có dấu móc ưu tiên thực hiện
Đối với trường hợp khi biến được truy xuất chỉ xác định dạng read (rd), dấu móc có thể bỏ qua.

↼
12
Đặc tả operation
Ví dụ
SHOW () r: N
ext rd reg: N
post r = reg



SHOW () r: N
ext rd reg: N
post r = reg

↼
13
Đặc tả operation
Ví dụ
SHOW () r: N
ext wr reg: N
post r = reg  r = reg

Dạng tổng quát
OP (p:Tp) r: Tr
ext rd v1: T1,
wr v2: T2,
pre …p…v1…v2…
post …p…v1…v2…r…v2…
↼
↼
14
Đặc tả operation
Ví dụ
ADD ( i : N)
ext wr reg: N
post reg = reg + i
↼
15
Đặc tả operation
Bức tranh của đặc tả operation

16
Đặc tả operation
Các phần đặc tả của một chương trình
FACT
ext wr n:N,
wr fn:N
post fn = n!
Nó được thực hiện bởi một đoạn sau đây của chương trình
fn := 1;
while n≠0 do
(fn := fn*n;
n:=n-1)
↼
17
Đặc tả operation
Người thiết kế chương trình có thể chia đặc tả chương trình FACT ra làm 2 phần là INIT và LOOP
INIT
ext wr fn:N
post fn = 1

LOOP
ext wr n:N,
wr fn : N
post fn = fn * n
↼
↼
18
Đặc tả operation
Ở bước tiếp theo, người thiết kế chương trình có thể chia đặc tả chương trình LOOP thành các phần nhỏ hơn như

While n ≠0 do BODY
BODY
ext wr n:N,
wr fn:N
pre n>0
post fn*n! = fn*n!  n↼
↼
↼