Trường Đại học Công Nghệ Thông Tin, ĐHQG-HCM
Khoa Công Nghệ Phần Mềm

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

PGS.TS. Vũ Thanh Nguyên

4/5/2019
CuuDuongThanCong.com

1
/>

Kiểu dữ liệu trong VDM
integer
values:
{-32768,…, 32767}
operations:
+, - , *, div, mod, =, <>, >, <, >=,
/>
3


Các tập hợp được định nghĩa sẵn

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
4


Các tập hợp được định nghĩa sẵn
Một kiểu dữ liệu bao gồm:
 Tập hợp các giá trị
 Hệ thống các phép toán cơ sở
Dựa trên các phép toán này, ta có thể đặc tả các phép toán còn lại.
Một phép toán (có thể được gọi là 1 hàm) là một ánh xạ riêng phần
trên tập D X, D là miền xác định của f:

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên


 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
4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
7


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

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên



4/5/2019

Ví dụ:
ext
ext

rd
wr
CuuDuongThanCong.com

size: ℕ
a, b: ℕ,

rd x: ℤ

PGS.TS. Vũ Thanh Nguyên

/>
10


Đặ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

↼

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
12


Đặ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.

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên


 SHOW () r: N
ext wr reg: N
post r = reg r = reg

↼

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
15


Đặc tả operation

 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…

↼

4/5/2019

CuuDuongThanCong.com


PGS.TS. Vũ Thanh Nguyên

/>
18


Đặc tả operation
 Nhận xét:
 Trong các operator LOAD, SHOW, ADD thì không có
operator nào có tiền điều kiện (pre-condition).
 Cú pháp cho phép chúng ta bỏ đi tiền điều kiện khi giả
định rằng đặc tả của chúng ta luôn đúng với mọi trường
hợp của biến đầu vào.

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
19


Đặc tả operation
 Bức tranh của đặc tả operation

4/5/2019




Đặ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

↼↼

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
22


Đặ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ư