Bài giảng Đặc tả hình thức - Chương 6: Kiểu đối tượng phức - Vũ Thanh Nguyên

4/5/2019 PGS.TS. Vũ Thanh Nguyên 1 Chương 6: Kiểu đối tượng phức 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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 3 Đặc tả kiểu đối tượng phức  Trong quá trình phát triển các ứng dụng, đối với các kiểu dữ liệu được hỗ trợ trong hệ thống không đủ sức mạnh để chúng ta đặc tả các bài toán phức tạp.  Đối với khái niệm trong ngôn ngữ lập trình thì chúng ta sử dụng cấu trúc dữ liệu để mô tả các đối tượng này và trong đặc tả hình thức chúng ta có khái niệm tương tự đó là đối tượng phức.  Với một đối tượng phức chúng ta có thể xử lý được nhiều thông tin hơn so với đối tượng có sẵn. CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 4 Đặ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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 5 Đặ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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 6 Đặ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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 7 Đặ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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 8 Đặ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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 9 Đặ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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 10 Đặ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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 11 Đặ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 : ℝ CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 12 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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 13 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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 14 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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 15 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}) CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 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 : ℕ 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 CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 17 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} CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 18 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  Ví dụ: d =  (d, date ↦ 1) 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 ⃐ ⃐ ⃐ CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 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 ps = mk-Phân-số (tử-số-mới, mẫu-số-mới) ⃐ ⃐ CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 20 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 =  (ps, tử-số ↦ tử-số-mới, mẫu-số ↦ mẫu-số-mới) ⃐ ⃐ ⃐ CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 21 Cập nhật đối tượng phức  Ví dụ: Sơ đồ của phép toán Datec CuuDuongThanCong.com https://fb.com/tailieudientucntt 4/5/2019 PGS.TS. Vũ Thanh Nguyên 22 Cập nhật đối tượng phức  Ví dụ: Hàm  cung cấp khả năng tạo giá trị kết hợp (phức) mà khác biệt chỉ ở một trường  dt = mk-Datec(17,1927)  (dt, day ↦ 29) = mk-Datec(29,1927)  (dt, year ↦ 1937) = mk-Datec(17,1937) CuuDuongThanCong.com https://fb.com/tailieudientucntt