Bài giảng Đặc tả hình thức - Chương 4: Đặc tả và tính đúng đắn của hàm - Nguyễn Trần Thi Văn

Nội dung text: Bài giảng Đặc tả hình thức - Chương 4: Đặc tả và tính đúng đắn của hàm - Nguyễn Trần Thi Văn

1. Đại học Sư phạm Kỹ thuật TP. HCM Khoa Công nghệ Thông tin o0o BÀI GIẢNG MÔN ĐẶC TẢ HÌNH THỨC Chương 4 Đặc tả và tính đúng đắn của hàm CBGD: Nguyễn Trần Thi Văn
2. Monday, June 14, 2021 Nội dung 1. Đặc tả và tính đúng đắn của hàm • Đặt vấn đề • Các phương pháp kiểm tra 2. Chứng minh với các luật suy diễn • Ký hiệu • Các luật suy diễn Đặc tả hình thức Đặc tả và tính đúng đắn 2
3. Monday, June 14, 2021 Giới thiệu • Ta xét hàm f với đặc tả như sau: f : X → Y x y Domain : P(x) Where: Q(x, y) Đặc tả hình thức Đặc tả và tính đúng đắn 3
4. Monday, June 14, 2021 Giới thiệu (2) • Có cài đặt tương ứng là: Y f(X) { lệnh 1; lệnh 2; lệnh 3; // } Đặc tả hình thức Đặc tả và tính đúng đắn 4
5. Monday, June 14, 2021 Giới thiệu (3) • Bài toán đặt ra ở đây là hãy cho biết cài đặt trên có phù hợp với đặc tả đã có hay không? • Đây chính là bài toán về kiểm tra tính đúng đắn của hàm. Nếu cài đặt cụ thể của hàm f là phù hợp với đặc tả, ta nói cài đặt đó là đúng, ngược lại, cài đặt đó là chưa chính xác. Đặc tả hình thức Đặc tả và tính đúng đắn 5
6. Monday, June 14, 2021 Giới thiệu (4) • Để kiểm tra tính đúng đắn của 1 hàm sau khi cài đặt, người ta sử dụng một số phương pháp khác nhau, hoặc cũng có thể kết hợp đồng thời các phương pháp này. • Có 2 phương pháp chính: – Kiểm tra động – Kiểm tra tĩnh Đặc tả hình thức Đặc tả và tính đúng đắn 6
7. Monday, June 14, 2021 Kiểm tra động • Phương pháp kiểm tra động (dynamic testing), hay còn được gọi là phương pháp thử nghiệm được thực hiện như sau : 1. Lập các bộ số làm thử nghiệm, hay còn được gọi là các bộ dữ liệu thử nghiệm (test cases). 2. Lần lượt cho thực hiện hàm f với các giá trị x đã chọn, ghi nhận lại kết quả y0. 3. So sánh y và y0. Đặc tả hình thức Đặc tả và tính đúng đắn 7
8. Monday, June 14, 2021 Kiểm tra động (2) • Phương pháp này chính là phương pháp kiểm thử chủ đạo được áp dụng trong giai đoạn lập trình và giai đoạn kiểm thử của quy trình phát triển phần mềm trên thế giới hiện nay. Đặc tả hình thức Đặc tả và tính đúng đắn 8
9. Monday, June 14, 2021 Kiểm tra động (3) • Các công cụ hỗ trợ phương pháp này: – Công cụ phát sinh các dữ liệu thử nghiệm. – Công cụ cho phép thực thi hàm và ghi nhận kết quả. – Công cụ kiểm tra tính phù hợp của cài đặt hàm so với đặc tả. – Các công cụ tự động phát sinh hàm từ đặc tả, cho thực hiện hàm phát sinh và tự động kiểm tra kết quả thực hiện. Đặc tả hình thức Đặc tả và tính đúng đắn 9
10. Monday, June 14, 2021 Kiểm tra động (4) • Phương pháp này còn được biết đến với 1 tên gọi khác là "kiểm thử hộp đen" (black box testing) • Phương pháp không chú trọng đến cài đặt bên trong của các hàm • Nó chỉ quan tâm đến kết quả thực hiện của hàm để khẳng định hàm đó có phù hợp với đặc tả không mà thôi • Chưa đề cập đến việc sửa chữa cài đặt của hàm lại sao cho phù hợp Đặc tả hình thức Đặc tả và tính đúng đắn 10
11. Monday, June 14, 2021 Kiểm tra tĩnh • Phương pháp kiếm tra tĩnh (static testing), còn được gọi là "kiểm thử hộp trắng" (white box testing). • Phương pháp này thực hiện theo cơ chế lần lượt đọc các lệnh trong chương trình nguồn (phần cài đặt của hàm) • Sau đó chứng minh bằng tay, hoặc chứng minh tự động tính đúng đắn của hàm sau từng lệnh. Đặc tả hình thức Đặc tả và tính đúng đắn 11
12. Monday, June 14, 2021 Kiểm tra tĩnh (2) • Ta xét hàm f với đặc tả và cài đặt: f : X → Y Y f(X) { x y lệnh 1; Domain : P(x) lệnh 2; Where: Q(x, y) lệnh k; } Đặc tả hình thức Đặc tả và tính đúng đắn 12
13. Monday, June 14, 2021 Kiểm tra tĩnh (3) • Ta xét các kết quả trung gian: – Q1(x,y): điều kiện sau khi thực hiện lệnh 1 – Q2(x,y): điều kiện sau khi thực hiện lệnh 2 – Q3(x,y): điều kiện sau khi thực hiện lệnh 3 – – Qk(x,y): điều kiện sau khi thực hiện lệnh k Đặc tả hình thức Đặc tả và tính đúng đắn 13
14. Monday, June 14, 2021 Kiểm tra tĩnh (4) • Các bước chứng minh: From P(x) Q1(x, y) lệnh 1 được thực hiện. Q2(x, y) lệnh 2 được thực hiện. Qk(x, y) lệnh k được thực hiện. Infer Q(x, y) Đặc tả hình thức Đặc tả và tính đúng đắn 14
15. Monday, June 14, 2021 Chứng minh với luật suy diễn • Cho E1, E2 là 2 mệnh đề. Trong quá trình chứng minh, nếu suy diễn được E1 thì cũng suy diễn được E2, ta ký hiệu: E1 E2 hay E1 E2 Đặc tả hình thức Đặc tả và tính đúng đắn 15
16. Monday, June 14, 2021 Chứng minh với luật suy diễn (2) • Cho E1, E2 là 2 mệnh đề. Trong quá trình chứng minh, nếu suy diễn được E1 thì cũng suy diễn được E2, ta ký hiệu: E1 E2 hay E1 E2 Đặc tả hình thức Đặc tả và tính đúng đắn 16
17. Monday, June 14, 2021 Chứng minh với luật suy diễn (2) • Nếu E 1 E 2 và E 2 E 1 thì ta ký hiệu: E1 E1 E2 E2 E1 E2 Đặc tả hình thức Đặc tả và tính đúng đắn 17
18. Monday, June 14, 2021 Các luật suy diễn • Suy diễn trên phép phủ định • Suy diễn trên phép hội • Suy diễn trên phép giao • Suy diễn trên phép kéo theo Đặc tả hình thức Đặc tả và tính đúng đắn 18
19. Monday, June 14, 2021 Suy diễn trên phép phủ định E E E ; (PĐ) E E E i.e: Tôi có nhà. Vậy: không thể có chuyện tôi không có nhà, và ngược lại. Đặc tả hình thức Đặc tả và tính đúng đắn 19
20. Monday, June 14, 2021 Các luật suy diễn • Suy diễn trên phép phủ định • Suy diễn trên phép hội • Suy diễn trên phép giao • Suy diễn trên phép kéo theo Đặc tả hình thức Đặc tả và tính đúng đắn 20
21. Monday, June 14, 2021 Suy diễn trên phép hội (1) Suy diễn MỞ RỘNG: E E ; ( _ MR) E  X X  E i.e: Tôi có nhà. Vậy: Tôi có nhà hay xe. Tôi có xe hay nhà. Đặc tả hình thức Đặc tả và tính đúng đắn 21
22. Monday, June 14, 2021 Suy diễn trên phép hội (2) Suy diễn THEO TRƯỜNG HỢP: E1 E2;E1 X ;E2 X ( _ TrH ) X i.e: Tôi có tiền hoặc vàng. Có tiền tôi sẽ có xe mới. Có vàng tôi cũng sẽ có xe mới. Vậy: Chắc chắn tôi sẽ có xe mới Đặc tả hình thức Đặc tả và tính đúng đắn 22
23. Monday, June 14, 2021 Suy diễn trên phép hội (3) Suy diễn DE MORGAN: (E1 E2) ( _ DE ) E2  E1 i.e: Tôi ko có tiền hay vàng gì cả. Vậy: Tôi không có tiền và cũng chẳng có vàng, và ngược lại. Đặc tả hình thức Đặc tả và tính đúng đắn 23
24. Monday, June 14, 2021 Suy diễn trên phép hội (4) Suy diễn KẾT HỢP: (E1 E2)  E3 ( _ KH) E1 (E2  E3) Đặc tả hình thức Đặc tả và tính đúng đắn 24
25. Monday, June 14, 2021 Các luật suy diễn • Suy diễn trên phép phủ định • Suy diễn trên phép hội • Suy diễn trên phép giao • Suy diễn trên phép kéo theo Đặc tả hình thức Đặc tả và tính đúng đắn 25
26. Monday, June 14, 2021 Suy diễn trên phép giao (1) Suy diễn THEO ĐỊNH NGHĨA: (E1 E2) ( _ ĐN) E1 E2 i.e: Tôi có cả xe lẫn nhà. Vậy: Không thể có chuyện tôi không có xe hoặc không có nhà, và ngược lại. Đặc tả hình thức Đặc tả và tính đúng đắn 26
27. Monday, June 14, 2021 Suy diễn trên phép giao (2) Suy diễn RÚT GỌN: E1 E2 ; E1 E2 ( _ RG ) E1 E2 i.e: Tôi có cả xe lẫn nhà. Vậy: Tôi chắc chắn có nhà. Tôi chắc chắn có xe. Đặc tả hình thức Đặc tả và tính đúng đắn 27
28. Monday, June 14, 2021 Suy diễn trên phép giao (3) Suy diễn TỔNG HỢP: E1; E2 ( _TH) E1 E2 i.e: Tôi có xe. Tôi cũng có nhà. Vậy: Tôi có cả xe lẫn nhà. Đặc tả hình thức Đặc tả và tính đúng đắn 28
29. Monday, June 14, 2021 Suy diễn trên phép giao (4) Suy diễn DE MORGAN: (E1 E2) ( _ DE ) E1 E2 i.e: Tôi ko có đồng thời cả tiền và vàng Vậy: Hoặc là tôi không có tiền, hoặc tôi chẳng có vàng, và ngược lại. Đặc tả hình thức Đặc tả và tính đúng đắn 29
30. Monday, June 14, 2021 Suy diễn trên phép giao (5) Suy diễn KẾT HỢP: (E1 E2)  E3 ( _ KH) E1 (E2  E3) Đặc tả hình thức Đặc tả và tính đúng đắn 30
31. Monday, June 14, 2021 Các luật suy diễn • Suy diễn trên phép phủ định • Suy diễn trên phép hội • Suy diễn trên phép giao • Suy diễn trên phép kéo theo Đặc tả hình thức Đặc tả và tính đúng đắn 31
32. Monday, June 14, 2021 Suy diễn trên phép kéo theo (1) Suy diễn BÀI TAM: (BT ) E  E Đặc tả hình thức Đặc tả và tính đúng đắn 32
33. Monday, June 14, 2021 Suy diễn trên phép kéo theo (2) Suy diễn DỰA TRÊN MÂU THUẪN: E  E (MT ) X Đặc tả hình thức Đặc tả và tính đúng đắn 33
34. Monday, June 14, 2021 Suy diễn trên phép kéo theo (3) Suy diễn KÉO THEO: E1 E2 ( _ ĐN) E1 E2 Đặc tả hình thức Đặc tả và tính đúng đắn 34
35. Monday, June 14, 2021 Suy diễn trên phép kéo theo (4) Suy diễn TƯƠNG ĐƯƠNG: (E1 E2)  (E2 E1) ( _ ĐN) E1 E2 Đặc tả hình thức Đặc tả và tính đúng đắn 35
36. Monday, June 14, 2021 Chứng minh suy diễn (1) • Khi chứng minh suy diễn E F ta áp dụng dạng thức sau: From E Kết quả 1 Luật suy diễn áp dụng(các kquả sd) Kết quả 2 Luật suy diễn áp dụng(các kquả sd) Infer F Đặc tả hình thức Đặc tả và tính đúng đắn 36
37. Monday, June 14, 2021 Chứng minh suy diễn (2) • Ví dụ: Chứng minh các suy diễn sau E1 E2 1. ( _ GH) E2  E1 E1;E2 2. ( _TH) (E1 E2) E1 (E2  E3) 3. ( _ PP) (E1 E2)  (E1 E3) E1 E2 4. ( _ GH) E2  E1 Đặc tả hình thức Đặc tả và tính đúng đắn 37
38. Monday, June 14, 2021 Bài tập áp dụng • Ví dụ: Chứng minh các suy diễn sau E1 (E2  E3) 1. ( _ PP) (E1 E2)  (E1 E3) (E1 E2)  (E1 E3) 2. ( _ PP) E1 (E2  E3) (E1 E2)  (E1 E3) 3. ( _ PP) E1 (E2  E3) E1 E2;E2 X 4. ( _ TT) E1 X Đặc tả hình thức Đặc tả và tính đúng đắn 38
39. Monday, June 14, 2021 Tóm tắt chương • Kiểm thử nhằm mục đích đảm bảo tính đúng đắn của hàm, của chương trình. • Có 2 phương pháp kiểm thử chính: kiểm thử động và kiểm thử tĩnh. • Chứng minh tính đúng đắn của hàm dựa vào các luật suy diễn. • Có các luật suy diễn trên phép phủ định, hội, giao, và kéo theo. Đặc tả hình thức Đặc tả và tính đúng đắn 39
40. Monday, June 14, 2021 HẾT CHƯƠNG 4 Đặc tả hình thức Đặc tả và tính đúng đắn 40