Bài giảng Đặc tả hình thức - Chương 3: Mô hình hóa dữ liệu kiểu tập hợp - Vũ Thanh Nguyên

1Chươ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 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 2Kiểu dữ liệu trong VDM integer values: {-32768,, 32767} operations: +, - , *, div, mod, =, , >, =, <= Các kiểu dữ liệu đơn giản được định nghĩa sẵn: ℕ, ℕ1, ℤ, ℝ, ℚ, B, Char 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 3Cá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/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 4Các tập hợp được định nghĩa sẵn 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 5Cá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 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 6Mô 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/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 7Kiể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 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 8Kiể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 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 9Kiể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 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 10 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: ℤ 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 11 Đặ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 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 12 Đặ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 ⃐ ↼ 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 13 Đặ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 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 14 Đặ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 ↼ 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 15 Đặc tả operation  Ví dụ  SHOW () r: N ext wr reg: N post r = reg r = reg↼ 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 16 Đặc tả operation  Dạng tổng quát  OP (p:Tp) r: Tr ext rd v1: T1, wr v2: T2, pre pv1v2 post pv1v2rv2 ↼ 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 17 Đặc tả operation  Ví dụ  ADD ( i : N) ext wr reg: N post reg = reg + i ↼ 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 18 Đặc tả operation 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 19 Đặ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 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 20 Đặc tả operation  Bức tranh của đặc tả operation 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 21 Đặ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) ↼ 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 22 Đặ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 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt 23 Đặ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ư phần bổ sung  While n ≠0 do BODY  BODY ext wr n:N, wr fn:N pre n>0 post fn*n! = fn*n! n<n ↼↼ ↼ 4/5/2019 PGS.TS. Vũ Thanh Nguyên CuuDuongThanCong.com https://fb.com/tailieudientucntt