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

1

Giảng viên: PGS.TS. Vũ Thanh Nguyên

Kiểu dữ liệu trong VDM

integer

values: {-32768,…, 32767}

operations: +, - , *, div, mod, =, <>, >, <, >=, <=

2

Các kiểu dữ liệu đơn giản được định nghĩa sẵn: ℕ, ℕ1, ℤ, ℝ, ℚ, B, Char

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

ℤ = {…, -2, -1, 0, 1, 2, …} ℕ = {0, 1, 2, 3, …} ℕ1 = {1, 2, 3, …} ℝ ℚ B = {true, false}

Tập số nguyên Tập số tự nhiên Tập số nguyên dương Tập số thực Tập số hữu tỉ Tập boolean Tập ký tự (gồm chữ cái hoa/thường, số, phép toán, dấu câu)

3

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’, ‘+’, ‘-’, ‘=‘, ‘<‘, ‘>’, ‘*’, ‘/’, ‘(‘, ‘)’, ‘[‘, ‘]’, ‘{‘, ‘}’, ‘.’, ‘,’, ‘?’, ‘!’, …}

Mô hình hóa dữ liệu

Technical-Staff

values: {PROJECT-MANAGER, TEAM-LEADER, ANALYST, DESIGNER, PROGRAMMER, TESTER}

operations:

Technical-Staff = {PROJECT-MANAGER, TEAM-LEADER, ANALYST, DESIGNER, PROGRAMMER, TESTER}

4

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:

5

Intset = ℤ-set

Kiểu tập hợp

 Ví dụ 3:

6

Pupils = { Patrick, Christa, Emma, Pete, Frank, Lisa, Richard, David, Daniel, John, Helen, Pauline, Mark, Mike, Elisabeth} School-trip = Pupils-set

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

7

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

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ả

 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

 Đối với các biến bên ngoài:

 Ví dụ: ext ext

8

rd wr size: ℕ a, b: ℕ, rd x: ℤ

Đặc tả operation

Tên_Operation (thamsố1: Kiểu1, thamsố2: Kiểu2…) kq: Kiểukq ext

9

wr BiếnRead_Write: Kiểu, rd BiếnRead_Only: Kiểu Vị từ pre-condition pre post Vị từ post-condition

Đặc tả operation

 Ví dụ

x: ℝ

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

10

trip: School-trip ↼ ADD-TO-TRIP (new-on-trip: School-trip) ext pre post wr  new-on-trip  trip trip = trip  new-on-trip

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

11

dạng read (rd), dấu móc có thể bỏ qua.

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

12

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

13

Đặc tả operation

 Ví dụ

 ADD ( i : N) ext wr reg: N post reg = reg + i ↼

14

Đặc tả operation

15

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

Đặc tả operation

 FACT

 Các phần đặc tả của một chương trình

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;

16

while n≠0 do (fn := fn*n; n:=n-1)

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

 LOOP

ext wr fn:N post fn = 1

ext wr n:N,

wr fn : N

17

post fn = fn * n↼ ↼

Đặc tả operation

 While n ≠0 do BODY  BODY

 Ở 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ư

ext wr n:N, wr fn:N

↼↼ ↼

18

pre n>0 post fn*n! = fn*n!  n