Bài giảng Đặc tả hình thức - Chương 7: Kiểu ánh xạ - Vũ Thanh Nguyên

1Chương 7 Kiểu ánh xạ 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 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 2Nội dung  Ánh xạ  Các hàm và thao tác trên ánh xạ  Đặc tả sử dụng ánh xạ 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 3Kiể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”, } 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 4Kiể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} 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 5Kiểu ánh xạ 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 6Á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 Tiền ảnh Ảnh 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 7Định nghĩa kiểu ánh xạ  Định nghĩa kiểu ánh xạ: A  B  Ví dụ 1: f : ℤ  ℤ  Ví dụ 2: Acc-system:: custs: Name  Acc-no accs: Acc-no  Account  Ví dụ 3: thuộc-khoa: SINH-VIÊN  KHOA  Ví dụ 4: phân-công: NHÂN-VIÊN  PHÒNG-BAN m m m m m m 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 8Đị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} 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 9Hàm và thao tác trên ánh xạ  Hàm Domain (dom) 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) 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 m m 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 10 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 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 11 Toán tử cập nhật †  Cho m và n là 2 ánh xạ cùng kiểu _†_ : A  B  A  B  A  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) } m m m 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 12 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} 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 13 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 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 14 Toán tử chọn các bộ theo tập khóa ⊲ _⊲_ : 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 m m 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 15 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 ⊲ {} = {} 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 16 Toán tử xóa bộ dựa vào tập khóa ⊲ _⊲_ : 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 _ m m _ _ _ _ 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 17 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 _ _ 4/5/2019 PGS.TS. Vu Thanh Nguyen _ _ CuuDuongThanCong.com https://fb.com/tailieudientucntt 18 Đặc tả với kiểu ánh xạ  Ví dụ: Mã-HP  Tên-HP Mã-GV  Mã-HP-set Mã-GV  Giảng-Viên Mã-SV  Sinh-Viên m m m m 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 19 Đặ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 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 20 Đặc tả với kiểu ánh xạ Đăng-ký = Sinh-Viên  Lớp-set Danh-sách-lớp= Lớp  Sinh-Viên-set m m 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 21 Đặc tả với kiểu ánh xạ  Ví dụ: Đặc tả hàm trả về các lớp mà sinh viên sv đã và đang đăng ký học DSĐăngKýHọc : Sinh-Viên  Đăng-ký  Đăng-ký DSĐăngKýHọc (sv, ds-đăng-ký) ≜ {sv} ⊲ ds-đăng-ký DSLớpĐăngKýHọc : Sinh-Viên  Đăng-ký  Lớp-set DSLớpĐăngKýHọc (sv, ds-đăng-ký) ≜ if (sv  dom ds-đăng-ký) then ds-đăng-ký(sv) else {} 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 22 Đặc tả với kiểu ánh xạ  Ví dụ: Đăng ký cho 1 sinh viên học 1 lớp ĐĂNG-KÝ-HỌC (sv: Sinh-Viên, lớp: Lớp) ext wr đk: Đăng-ký pre ({sv} ⊲ đk = {})  (lớp  ({sv} ⊲ đk)(sv)) post (đk = đk † { sv ↦ ({sv} ⊲ đk )(sv)  {lớp}) }  ({sv} ⊲ đk  {}))  (đk = đk  { sv ↦ {lop})  ({sv} ⊲ đk = {})) ↼ ↼ ↼ ↼ ↼ ↼ ↼ 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt 23 Đặc tả với kiểu ánh xạ  Ví dụ: Đăng ký cho 1 sinh viên học 1 lớp ĐĂNG-KÝ-HỌC (sv: Sinh-Viên, lớp: Lớp) ext wr đk: Đăng-ký pre (sv  dom(đk))  ((sv  dom(đk))  (lớp  đk(sv))) post ((đk = đk † { sv ↦ đk(sv)  {lớp}})  (sv  dom(đk)))  ((đk = đk  { sv ↦ {lop})  (sv  dom(đk))) ↼ ↼ ↼ ↼ ↼ ↼ ↼ ↼ 4/5/2019 PGS.TS. Vu Thanh Nguyen CuuDuongThanCong.com https://fb.com/tailieudientucntt