Trang chủ » Công Nghệ Thông Tin » Kỹ thuật phần mềm

21 trang

29 lượt xem

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!

bapnep06

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

23-02-2023

TS. Vũ Thanh Nguyên

Nội dung

23-02-2023

TS. Vũ Thanh Nguyên

 Đị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

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

 Cú pháp:

Tên-kiểu-đối-tượng-phức ::

23-02-2023

TS. Vũ Thanh Nguyên

Tên-field1: Kiểu1 Tên-field2: Kiểu2 … Tên-fieldn: Kiểun

Đặ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 :: …

 Lưu ý: ký hiệu :: thường được sử dụng hơn so với

Name = compose Name of … end

23-02-2023

TS. Vũ Thanh Nguyên

compose

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

 Ví dụ: xác đinh kiẻu dữ liệu Datec

Datec ::

day year : {1,…,366} : N

hoặc

Datec = compose Datec of : {1,…,366} : N day year

23-02-2023

TS. Vũ Thanh Nguyên

end

Đặ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

23-02-2023

TS. Vũ Thanh Nguyên

end

Đặ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ố : ℤ

23-02-2023

TS. Vũ Thanh Nguyên

end

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

 Ví dụ:

Khách-hàng :: : String họ-tên đị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

23-02-2023

TS. Vũ Thanh Nguyên

end

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

 Ví dụ:

Date = compose Date of

: {d  ℕ1 | d  31} day month : {m ℕ1 | m  12} year : {y  ℕ1 | y  1900}

end

 Ví dụ:

Date = compose Date of

: {1, 2, …, 31} day month : {1, 2, …, 12} year : {y  ℕ1 | y  1900}

23-02-2023

TS. Vũ Thanh Nguyên

end

Đặ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 ::

23-02-2023

TS. Vũ Thanh Nguyên

tâm : Điểm bán-kính : ℝ

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ụ:

23-02-2023

TS. Vũ Thanh Nguyên

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

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)

23-02-2023

TS. Vũ Thanh Nguyên

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

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ữ

 Ràng buộc trên 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

liệu

trong 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

 Ví dụ: mk-Date (29, 2, 2007) !!!  Ràng buộc trên kiểu dữ liệu

23-02-2023

TS. Vũ Thanh Nguyên

bảo tính hợp lệ của thông tin trong đối tượng

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 :: : {d  ℕ1 | d  31} day 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})

23-02-2023

TS. Vũ Thanh Nguyên

 (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})

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) ≜

23-02-2023

TS. Vũ Thanh Nguyên

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

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) ≜

23-02-2023

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

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

23-02-2023

TS. Vũ Thanh Nguyên

giữa nguyên giá trị tháng và năm

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)

ps: Phân-số

⃐

23-02-2023

TS. Vũ Thanh Nguyên

RÚT-GỌN-PS ext wr ⃐ 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)

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)

ps: Phân-số

⃐

RÚT-GỌN-PS ext wr ⃐ 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)