[Bài Giảng] Chương 4: Đặc tả và tính đúng đắn của hàm

Chương 4 : Đặc tả và tính đúng đắn của hàm

Nội dung

• Đặc tả và tính đúng đắn của hàm

1. Đặt vấn đề
2. Các phương pháp kiểm tra

• Chứng minh với các luật suy diễn

1. Ký hiệu
2. Các luật suy diễn

Giới thiệu

Ta xét hàm f với đặc tả như sau:

Domain : P(x)
Where: Q(x, y)

Có cài đặt tương ứng là:
Y f(X)
{
lệnh 1;
lệnh 2;
lệnh 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.

• Để 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:

1. Kiểm tra động
2. Kiểm tra tĩnh

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ả y.
3. So sánh y và y0. 

• 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ác công cụ hỗ trợ phương pháp này:

1. Công cụ phát sinh các dữ liệu thử nghiệm.
2. Công cụ cho phép thực thi hàm và ghi nhận kết quả.
3. Công cụ kiểm tra tính phù hợp của cài đặt hàm so với đặc tả.
4. 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.  

• 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 

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.

Ta xét hàm f với đặc tả và cài đặt:

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

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:

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

Suy diễn trên phép phủ định

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ác luật suy diễn

1. Suy diễn trên phép phủ định
2. Suy diễn trên phép hội
3. Suy diễn trên phép giao
4. Suy diễn trên phép kéo theo

Suy diễn trên phép hội 

Suy diễn MỞ RỘNG:

i.e: Tôi có nhà.
Vậy: Tôi có nhà hay xe.
 Tôi có xe hay nhà.

Suy diễn THEO TRƯỜNG HỢP:

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

Suy diễn DE MORGAN:

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.

Suy diễn KẾT HỢP:

Suy diễn trên phép giao

Suy diễn THEO ĐỊNH NGHĨA:

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.

Suy diễn RÚT GỌN:



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.

Suy diễn TỔNG HỢP:

i.e: Tôi có xe.
Tôi cũng có nhà.
Vậy: Tôi có cả xe lẫn nhà.

Suy diễn DE MORGAN:

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.

Suy diễn KẾT HỢP:

Suy diễn trên phép kéo theo

Suy diễn BÀI TAM:

Suy diễn DỰA TRÊN MÂU THUẪN:

Suy diễn KÉO THEO:

Suy diễn KÉO THEO 2 CHIỀU:

Chứng minh suy diễn 

Khi chứng minh suy diễn
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

Ví dụ: Chứng minh các suy diễn sau

Bài tập áp dụng
Ví dụ: Chứng minh các suy diễn sau

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.

HẾT CHƯƠNG 4