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

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

PGS.TS. Vũ Thanh Nguyên

4/5/2019
CuuDuongThanCong.com

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

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
2


Đặc tả kiểu đối tượng phức


CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
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 :: …



4/5/2019

Name = compose Name of … end
Lưu ý: ký hiệu :: thường được sử dụng hơn so với
compose

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
5


hay
Celsius = compose Celsius of
v
: R

end

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
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

4/5/2019


Đặ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
4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
10


Đặc tả kiểu đối tượng phức
 Ví dụ:
Điểm ::
x:ℝ
y:ℝ


/>
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

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
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

4/5/2019

CuuDuongThanCong.com

PGS.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 : ℕ
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
4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>

 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

4/5/2019

CuuDuongThanCong.com

PGS.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



4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
20


Cập nhật đối tượng phức
 Ví dụ: Sơ đồ của phép toán Datec

4/5/2019

CuuDuongThanCong.com

PGS.TS. Vũ Thanh Nguyên

/>
21


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)


Nhờ tải bản gốc

Tài liệu, ebook tham khảo khác

Music ♫

Copyright: Tài liệu đại học © DMCA.com Protection Status