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

Bài giảng Đặc tả hình thức: Chương 7 Kiểu ánh xạ, cung cấp cho người đọc những kiến thức như: Ánh xạ; Các hàm và thao tác trên ánh xạ; Đặc tả sử dụng ánh xạ. 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 7 - 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 7 Kiểu ánh xạ TS. Vũ Thanh Nguyên 23-02-2023 TS. Vu Thanh Nguyen 1 Nội dung  Ánh xạ  Các hàm và thao tác trên ánh xạ  Đặc tả sử dụng ánh xạ 23-02-2023 TS. Vu Thanh Nguyen 2 Kiểu ánh xạ  Ví dụ: { “TH301” ↦ “Đặc tả hình thức”, “TH402” ↦ “Công cụ và Môi trường phát triển phần mềm”, “TH403” ↦ “Xây dựng phần mềm hướng đối tượng”, …} 23-02-2023 TS. Vu Thanh Nguyen 3 Kiểu ánh xạ  Nhắc lại:  Tích Descarte: A  B = {(a, b) | (a  A)  (b B)}  Ánh xạ và tích Descarte:  Cho A = {a1, a2, a3, a4, …}, B = {b1, b2, b3, …} {(a1, b1), (a2, b2), (a3, b1), (a4, b3)}  A  B  Khi đó, ta có ánh xạ từ A vào B sau: {a1↦ b1, a2 ↦ b2, a3 ↦ b1, a4 ↦ b3} 23-02-2023 TS. Vu Thanh Nguyen 4 Ánh xạ  Đơn ánh: Mỗi phần tử trong tập nguồn tương ứng với tối đa 1 phần tử (ảnh) trong tập đích  Toàn ánh: Mỗi phần tử trong tập nguồn đều có ảnh trong tập đích  Song ánh: Mỗi phần tử trong tập đích có duy nhất một tiền ảnh trong tập nguồn Tập nguồn Tập đích Ảnh Tiền ảnh 23-02-2023 TS. Vu Thanh Nguyen 5 Định nghĩa kiểu ánh xạ m  Định nghĩa kiểu ánh xạ: A  B  Ví dụ 1: m f:ℤ ℤ  Ví dụ 2: Acc-system:: m custs: Name  Acc-no accs: Acc-no  m Account  Ví dụ 3: m thuộc-khoa: SINH-VIÊN  KHOA  Ví dụ 4: phân-công: NHÂN-VIÊN m  PHÒNG-BAN 23-02-2023 TS. Vu Thanh Nguyen 6 Định nghĩa ánh xạ  Định nghĩa ánh xạ thông qua tính chất: {x ↦ y | Vị từ liên quan đến x và y}  Ví dụ: {p ↦ q | (p = 1  q = TRUE)  (p = 0  q = FALSE)} chính là {1 ↦ TRUE, 0 ↦ FALSE} 23-02-2023 TS. Vu Thanh Nguyen 7 Hàm và thao tác trên ánh xạ  Hàm Domain (dom) m dom: A  B  A-set dom(m) ≝ { a |  b  B  ( (a ↦ b)  m)}  Ý nghĩa: tập các phần tử trong tập nguồn A có ảnh trong tập đích B  Hàm Range (rng) m rng: A  B  B-set rng (m) ≝ { b |  a  A  ( (a ↦ b)  m)}  Ý nghĩa: tập các phần tử trong tập đích B có tiền ảnh trong tập nguồn A 23-02-2023 TS. Vu Thanh Nguyen 8 Hàm và thao tác trên ánh xạ  Ví dụ: vowel {‘A’ ↦ 65, ‘E’ ↦ 69, ‘I’ ↦ 73, ‘O’ ↦ 79, ‘U’ ↦ 85} dom (vowel) = {‘A’, ‘E’, ‘I’, ‘O’, ‘U’} rng (vowel) = {65, 69, 73, 79, 85} vowel(‘A’) = 65 vowel(‘U’) = 85 23-02-2023 TS. Vu Thanh Nguyen 9 Toán tử cập nhật †  Cho m và n là 2 ánh xạ cùng kiểu _†_ : A m B  Am B  A m B m †n ≝ {a↦b| (( a  dom n)  (b = n(a)))  ((a  (dom m – dom n))  (b = m(a))} hoặc {a↦ (if a  dom n then n(a) else m(a) | a  (dom m  dom n) } 23-02-2023 TS. Vu Thanh Nguyen 10 Toán tử cập nhật †  Kết quả của m † n là tập hợp tất cả các bộ trong n và các bộ trong m không có tiền ảnh/khóa trong dom(n)  Ví dụ: { 2 ↦ 4, 1 ↦ 3} † {3 ↦ 5, 1 ↦ 2} = {1 ↦2, 2 ↦ 4, 3 ↦ 5} { 3 ↦ 5, 1 ↦ 2} † {2 ↦ 4, 1 ↦ 3} = {1 ↦3, 2 ↦ 4, 3 ↦ 5} 23-02-2023 TS. Vu Thanh Nguyen 11 Giả sử m1 = {a ↦ 1, c ↦ 3, d ↦ 1}, m2 = {b ↦ 4, c ↦ 5} m1†m2 = {a ↦ 1,b ↦ 4, c ↦ 5,d ↦ 1} m2†m1 = {a ↦ 1,b ↦ 4, c ↦ 3,d ↦ 1} m†{} = m = {}†m 23-02-2023 TS. Vu Thanh Nguyen 12 Toán tử chọn các bộ theo tập khóa ⊲ m m _⊲ _ : A-set  A B  A B s⊲m≝ { a ↦ m(a) | a  (dom m  s ) }  Ý nghĩa: chọn lại những bộ trong ánh xạ có giá trị khóa cho trước 23-02-2023 TS. Vu Thanh Nguyen 13 Toán tử chọn các bộ theo tập khóa ⊲  Ví dụ: { 2, 3, 4} ⊲ {1 ↦ 3, 4 ↦ 7, 3 ↦ 3} = {4 ↦ 7, 3 ↦ 3} { a, d, e} ⊲ m1 = {a ↦ 1, d ↦ 1} {} ⊲ m = {} s ⊲ {} = {} 23-02-2023 TS. Vu Thanh Nguyen 14 Toán tử xóa bộ dựa vào tập khóa ⊲_ m m _⊲_ _ : A-set  A B  A B s ⊲_ m ≝ { a ↦ m(a) | a  (dom m – s ) }  Ý nghĩa: Xóa bỏ các bộ trong ánh xạ có giá trị khóa cho trước _ _ 23-02-2023 TS. Vu Thanh Nguyen 15 Toán tử xóa bộ dựa vào tập khóa ⊲_ Ví dụ: { 2, 3, 4} ⊲_ {1 ↦ 3, 4 ↦ 7, 3 ↦ 3} = {1 ↦ 3} { a, d, e} ⊲_ m1 = {c ↦ 3} {} ⊲_ m = m ma†mb = (dom mb – ma)  mb 23-02-2023 TS. Vu Thanh Nguyen 16 Đặc tả với kiểu ánh xạ  Ví dụ: m Mã-HP  Tên-HP m Mã-GV  Mã-HP-set m Mã-GV  Giảng-Viên m Mã-SV  Sinh-Viên 23-02-2023 TS. Vu Thanh Nguyen 17 Đặc tả với kiểu ánh xạ  Ví dụ: Mã-HP = Char* Mã-SV = Char* HọTên = Char* Sinh-Viên :: mã-SV: Mã-SV họ-tên: HọTên Lớp :: mã-HP: Mã-HP mã-Lớp: ℕ1 học-kỳ: {1, 2, 3, 4} năm-học: ℕ1 23-02-2023 TS. Vu Thanh Nguyen 18 Đặc tả với kiểu ánh xạ m Đăng-ký = Sinh-Viên  Lớp-set m Danh-sách-lớp= Lớp  Sinh-Viên-set 23-02-2023 TS. Vu Thanh Nguyen 19 ...