Bài giảng Đặc tả hình thức: Chương 6 - PGS.TS. Vũ Thanh Nguyên
lượt xem 3
download
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!
Bình luận(0) Đăng nhập để gửi bình luận!
Nội dung Text: 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 = 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
- 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
- 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
- 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
- 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
CÓ THỂ BẠN MUỐN DOWNLOAD
-
Bài giảng Đặc tả hình thức: Chương 2 - Nguyễn Thị Minh Tuyền
43 p | 66 | 9
-
Bài giảng Đặc tả hình thức: Chương 3 - Nguyễn Thị Minh Tuyền
69 p | 80 | 7
-
Bài giảng Đặc tả hình thức: Chương 4 - Nguyễn Thị Minh Tuyền
24 p | 80 | 7
-
Bài giảng Đặc tả hình thức: Chương 8 - Nguyễn Thị Minh Tuyền
33 p | 67 | 5
-
Bài giảng Đặc tả hình thức: Chương 1 - Nguyễn Thị Minh Tuyền
40 p | 54 | 5
-
Bài giảng Đặc tả hình thức: Chương 2 - PGS.TS. Vũ Thanh Nguyên
75 p | 8 | 3
-
Bài giảng Đặc tả hình thức: Chương 3 - PGS.TS. Vũ Thanh Nguyên
18 p | 5 | 3
-
Bài giảng Đặc tả hình thức: Chương 5 - PGS.TS. Vũ Thanh Nguyên
46 p | 4 | 3
-
Bài giảng Đặc tả hình thức: Chương 7 - PGS.TS. Vũ Thanh Nguyên
22 p | 11 | 3
-
Bài giảng Đặc tả hình thức: Chương 0 - Nguyễn Thị Minh Tuyền
12 p | 67 | 3
-
Bài giảng Đặc tả hình thức: Chương 1 - PGS.TS. Vũ Thanh Nguyên
21 p | 8 | 3
-
Bài giảng Đặc tả hình thức: Chương 0 - PGS.TS. Vũ Thanh Nguyên
6 p | 10 | 3
-
Bài giảng Đặc tả hình thức: Chương 15 - Nguyễn Thị Minh Tuyền
25 p | 80 | 3
-
Bài giảng Đặc tả hình thức: Chương 11 - Nguyễn Thị Minh Tuyền
20 p | 75 | 3
-
Bài giảng Đặc tả hình thức: Chương 10 - Nguyễn Thị Minh Tuyền
28 p | 88 | 3
-
Bài giảng Đặc tả hình thức: Chương 9 - Nguyễn Thị Minh Tuyền
22 p | 68 | 3
-
Bài giảng Đặc tả hình thức: Chương 8 - PGS.TS. Vũ Thanh Nguyên
47 p | 7 | 3
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