intTypePromotion=1
zunia.vn Tuyển sinh 2024 dành cho Gen-Z zunia.vn zunia.vn
ADSENSE
 » 
 » 

Bài giảng Đặc tả hình thức: Chương 3 - PGS.TS. Vũ Thanh Nguyên

Chia sẻ: _ _ | Ngày: | Loại File: PDF | Số trang:18

Thêm vào BST
Báo xấu
7
lượt xem 3
download
 
  Download Vui lòng tải xuống để xem tài liệu đầy đủ

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, cung cấp cho người đọc những kiến thức như: Kiểu dữ liệu trong VDM; Các tập hợp được định nghĩa sẵn; Mô hình hóa dữ liệu; Kiểu tập hợp; Mô hình hóa các operation; Đặc tả operation. Mời các bạn cùng tham khảo!

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: Bài giảng Đặc tả hình thức: Chương 3 - PGS.TS. Vũ Thanh Nguyên

  1. 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 1
  2. 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 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’, ‘+’, ‘-’, ‘=‘, ‘’, ‘*’, ‘/’, ‘(‘, ‘)’, ‘[‘, ‘]’, ‘{‘, ‘}’, ‘.’, ‘,’, ‘?’, ‘!’, …} 3
  4. 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
  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 5
  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 6
  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 7
  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: ℤ 8
  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 9
  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 10
  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. 11
  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 12
  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… 13
  14. Đặc tả operation  Ví dụ  ADD ( i : N) ext wr reg: N ↼ post reg = reg + i 14
  15. Đặc tả operation  Bức tranh của đặc tả operation 15
  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) 16
  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 17
  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
ADSENSE

CÓ THỂ BẠN MUỐN DOWNLOAD

THÔNG TIN
TRỢ GIÚP
HỖ TRỢ KHÁCH HÀNG
Theo dõi chúng tôi

Chịu trách nhiệm nội dung:

Nguyễn Công Hà - Giám đốc Công ty TNHH TÀI LIỆU TRỰC TUYẾN VI NA

LIÊN HỆ

Địa chỉ: P402, 54A Nơ Trang Long, Phường 14, Q.Bình Thạnh, TP.HCM

Hotline: 093 303 0098

Email: support@tailieu.vn

Giấy phép Mạng Xã Hội số: 670/GP-BTTTT cấp ngày 30/11/2015 Copyright © 2022-2032 TaiLieu.VN. All rights reserved.

 

Đồng bộ tài khoản
2=>2