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

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!
Nội dung trích xuất từ tài liệu:
Bài giảng Đặc tả hình thức: Chương 6 - 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 Chương 6: Kiểu đối tượng phức TS. Vũ Thanh Nguyên 23-02-2023 TS. Vũ Thanh Nguyên 1 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 Đặ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 Đặ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 Đặ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 Đặ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 Đặ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 Đặ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 Đặ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 Đặ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 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 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 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 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 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 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 ...