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 6 - PGS.TS. Vũ Thanh Nguyên

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

5
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 6 Kiểu đối tượng phức, cung cấp cho người đọc những kiến thức như: Định nghĩa kiểu đối tượng phức; Khởi tạo đối tượng phức; Ràng buộc trên kiểu dữ liệu; Cập nhật đối tượng phức. Mời các bạn cùng tham khảo!

Chủ đề:
Lưu

Nội dung Text: Bài giảng Đặc tả hình thức: Chương 6 - 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 6: Kiểu đối tượng phức TS. Vũ Thanh Nguyên 23-02-2023 TS. Vũ Thanh Nguyên 1
  2. Nội dung  Định nghĩa kiểu đối tượng phức  Khởi tạo đối tượng phức  Ràng buộc trên kiểu dữ liệu  Cập nhật đối tượng phức 23-02-2023 TS. Vũ Thanh Nguyên 2
  3. Đặc tả kiểu đối tượng phức  Cú pháp: Tên-kiểu-đối-tượng-phức :: Tên-field1: Kiểu1 Tên-field2: Kiểu2 … Tên-fieldn: Kiểun 23-02-2023 TS. Vũ Thanh Nguyên 3
  4. Đặc tả kiểu đối tượng phức  Ở đó:  ký hiệu :: có thể được đọc là ”is composed of” mà có thể định nghĩa tương đương 2 khả năng sau: Name :: … Name = compose Name of … end  Lưu ý: ký hiệu :: thường được sử dụng hơn so với compose 23-02-2023 TS. Vũ Thanh Nguyên 4
  5. Đặc tả kiểu đối tượng phức  Ví dụ: xác đinh kiẻu dữ liệu Datec Datec :: day : {1,…,366} year : N hoặc Datec = compose Datec of day : {1,…,366} year : N end 23-02-2023 TS. Vũ Thanh Nguyên 5
  6. Đặc tả kiểu đối tượng phức  Ví dụ: xác đinh kiẻu dữ liệu Fahrenheit và Celsius Fahrenheit = compose Fahrenheit of v : R end hay Celsius = compose Celsius of v : R end 23-02-2023 TS. Vũ Thanh Nguyên 6
  7. Đặc tả kiểu đối tượng phức  Ví dụ: Phân-số :: tử-số : ℤ mẫu-số : ℤ hoặc Phân-số = compose Phân-số of tử-số : ℤ mẫu-số : ℤ end 23-02-2023 TS. Vũ Thanh Nguyên 7
  8. Đặc tả kiểu đối tượng phức  Ví dụ: Khách-hàng :: họ-tên : String địa-chỉ : String điện-thoại: String hoặc Khách-hàng = compose Khách-hàng of họ-tên : String địa-chỉ : String điện-thoại: String end 23-02-2023 TS. Vũ Thanh Nguyên 8
  9. Đặc tả kiểu đối tượng phức  Ví dụ: Date = compose Date of day : {d  ℕ1 | d  31} month : {m ℕ1 | m  12} year : {y  ℕ1 | y  1900} end  Ví dụ: Date = compose Date of day : {1, 2, …, 31} month : {1, 2, …, 12} year : {y  ℕ1 | y  1900} end 23-02-2023 TS. Vũ Thanh Nguyên 9
  10. Đặc tả kiểu đối tượng phức  Ví dụ: Điểm :: x:ℝ y:ℝ Tam-giác :: A : Điểm B : Điểm C : Điểm Hình-tròn :: tâm : Điểm bán-kính : ℝ 23-02-2023 TS. Vũ Thanh Nguyên 10
  11. Tạo đối tượng phức  Hàm mk-TênKiểuĐốiTượngPhức dùng để tạo đối tượng phức thuộc kiểu tương ứng  Ví dụ: mk-Phân-số: ℤ  ℤ  Phân-số mk-Phân-số (5, 10) sẽ tạo ra 1 đối tượng phân số có tử-số là 5 và mẫu-số là 10 Điểm 23-02-2023 TS. Vũ Thanh Nguyên 11
  12. Tạo đối tượng phức  Ví dụ: mk-Điểm: ℝ  ℝ  Điểm mk-Tam-giác: Điểm  Điểm  Điểm  Tam-giác mk-Tam-giác (mk-Điểm(0,0), mk-Điểm (1,0), mk-Điểm(0, 1)) sẽ tạo ra tam giác có các điểm là A(0,0), B(1, 0) và C(0,1) mk-Hình-tròn: Điểm  ℝ  Hình-tròn mk-Hình-tròn (mk-Điểm(100,100), 200) sẽ tạo ra 1 đối tượng hình tròn có tâm (100,100) và bán kính 200 23-02-2023 TS. Vũ Thanh Nguyên 12
  13. Ràng buộc trên kiểu dữ liệu  Ràng buộc trên kiểu dữ liệu  Điều kiện về miền giá trị của các thuộc tính trong kiểu dữ liệu  Điều kiện về mối liên quan về giá trị của các thuộc tính trong kiểu dữ liệu  Ví dụ: mk-Date (29, 2, 2007) !!!  Ràng buộc trên kiểu dữ liệu  Tính chất bất biến (invariant) trên các thuộc tính nhằm đảm bảo tính hợp lệ của thông tin trong đối tượng 23-02-2023 TS. Vũ Thanh Nguyên 13
  14. Ràng buộc trên kiểu dữ liệu  Hàm kiểm tra ràng buộc trên kiểu dữ liệu  Ví dụ: Date :: day : {d  ℕ1 | d  31} month : {m ℕ1 | m  12} year : {y  ℕ1 | y  1900} inv-Date: Date  B inv-Date (d) ≜ (d.month  {1, 3, 5, 7, 8, 10, 12}  d.day  {1,…, 31})  (d.month  {4, 6, 9, 11}  d.day  {1,…, 30})  (d.month = 2  là-năm-nhuận(d.year)  d.day  {1,…, 29})  (d.month = 2  (là-năm-nhuận(d.year))  d.day  {1,…, 28}) 23-02-2023 TS. Vũ Thanh Nguyên 14
  15. Ràng buộc trên kiểu dữ liệu  Ví dụ: cho kiểu dữ liệu Mảng-tăng Mảng-tăng :: ds : ℝ* số-pt : ℕ Ràng buộc: mảng có tối đa 1000 phần tử, các phần tử trong ds luôn có thứ tự tăng và số-pt bằng đúng với số phần tử trong ds inv-Mảng-tăng: Mảng-tăng  B inv-Mảng-tăng (m) ≜ let s = m.ds, n = m.số-pt in len s  1000   i, j  inds s  i > j  s(i)  s(j)  n = len s 23-02-2023 TS. Vũ Thanh Nguyên 15
  16. Ràng buộc trên kiểu dữ liệu  Ví dụ: cho kiểu dữ liệu Mảng-tăng Mảng-tăng :: ds : ℝ* số-pt-không-âm-phân-biệt : ℕ Ràng buộc: các phần tử trong ds luôn có thứ tự tăng và số-pt- không-âm-phân-biệt là số lượng các phần tử không âm phân biệt trong ds inv-Mảng-tăng: Mảng-tăng  B inv-Mảng-tăng (m) ≜ let s = m.ds, n = m.số-pt in  i, j  inds s  i > j  s(i)  s(j)  n = card { x  elems s | x  0} 23-02-2023 TS. Vũ Thanh Nguyên 16
  17. Cập nhật đối tượng phức  Phương án 1: Tạo ra đối tượng mới với các thông tin mới cập nhật và các thông tin sẵn có ⃐  Ví dụ: d = mk-Date (1, d.month, ⃐ d.year) sẽ cập nhật lại giá trị ngày là 1, vẫn giữa nguyên giá trị tháng và năm  Phương án 2: sử dụng hàm  để cập nhật thuộc tính trong đối tượng phức ⃐ date ↦ 1) sẽ cập nhật lại giá trị ngày là 1, vẫn  Ví dụ: d =  (d, giữa nguyên giá trị tháng và năm 23-02-2023 TS. Vũ Thanh Nguyên 17
  18. Cập nhật đối tượng phức  Ví dụ: đặc tả hàm rút gọn phân số (giả sử tử số và mẫu số đều là số tự nhiên) RÚT-GỌN-PS ext wr ps: Phân-số ⃐ let tử-số-cũ = ps.tử-số, ⃐ mẫu-số-cũ = ps.mẫu-số in let u = uscln (tử-số-cũ, mẫu-số-cũ) in let tử-số-mới = tử-số-cũ / u, mẫu-số-mới = mẫu-số-cũ / u in ps = mk-Phân-số (tử-số-mới, mẫu-số-mới) 23-02-2023 TS. Vũ Thanh Nguyên 18
  19. Cập nhật đối tượng phức  Ví dụ: đặc tả hàm rút gọn phân số (giả sử tử số và mẫu số đều là số tự nhiên) RÚT-GỌN-PS ext wr ps: Phân-số ⃐ let tử-số-cũ = ps.tử-số, ⃐ mẫu-số-cũ = ps.mẫu-số in let u = uscln (tử-số-cũ, mẫu-số-cũ) in let tử-số-mới = tử-số-cũ / u, mẫu-số-mới = mẫu-số-cũ / u in ⃐ tử-số ↦ tử-số-mới, mẫu-số ↦ mẫu-số-mới) ps =  (ps, 23-02-2023 TS. Vũ Thanh Nguyên 19
  20. Cập nhật đối tượng phức  Ví dụ: Sơ đồ của phép toán Datec 23-02-2023 TS. Vũ Thanh Nguyên 20
ADSENSE

CÓ THỂ BẠN MUỐN DOWNLOAD

 

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