Chuong 4
CHƯƠNG IV: ĐẶC TẢ VÀ TÍNH ĐÚNG ĐẮN CỦA HÀM
Các nội dung chính của chương:
CHƯƠNG IV: ĐẶC TẢ VÀ TÍNH ĐÚNG ĐẮN CỦA HÀM... 1
IV.1 CÁC PHƯƠNG PHÁP KIỂM TRA TÍNH ĐÚNG ĐẮN.. 2
IV.1.1 Đặt vấn đề. 2
IV.1.2 Kiểm tra động. 2
IV.1.3 Kiểm tra tĩnh. 3
IV.2 CHỨNG MINH VỚI CÁC LUẬT SUY DIỄN.. 3
IV.2.1 Mở đầu. 3
IV.2.2 Các luật suy diễn. 4
IV.2.2.1 Các luật suy diễn trên phép phủ định (Ø). 4
IV.2.2.2 Các luật suy diễn trên phép hội (Ú). 4
IV.2.2.3 Các luật suy diễn trên phép tuyển (Ù). 5
IV.2.2.4 Các luật suy diễn trên phép kéo theo (Þ). 6
IV.2.3 Chứng minh luật suy diễn. 6
IV.2.3.1 Dạng thức :6
IV.2.3.2 Ví dụ. 6
IV.3 BÀI TẬP ÁP DỤNG.. 7
IV.1 CÁC PHƯƠNG PHÁP KIỂM TRA TÍNH ĐÚNG ĐẮN
IV.1.1 Đặt vấn đề
Ta xét hàm f với đặc tả như sau:
Domain : P(x)
Where: Q(x, y)
Với cài đặt tương ứng:
Y f(X)
{
//…
}
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. Trong các phần tiếp theo của chương, chúng tôi sẽ giới thiệu các tiếp cận của 1 số phương pháp phổ biến hiện nay.
IV.1.2 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 case) : .
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.
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 kiểm tra động (thử nghiệm) :
vCông cụ phát sinh các dữ liệu thử nghiệm.
vCông cụ cho phép thực thi hàm và ghi nhận kết quả.
vCông cụ kiểm tra tính phù hợp của cài đặt hàm so với đặc tả.
vCá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. Những công cụ tự động dạng này hiện vẫn chưa phổ biến, số lượng lẫn chất lượng của các công cụ này vẫn chưa đáp ứng được sự mong đợi của giới Công nghệ phần mềm.
vPhương pháp kiểm tra động 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), vì 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, hoàn toàn 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.
IV.1.3 Kiểm tra tĩnh
Phương pháp kiếm tra tĩnh, 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 mình bằng tay, hoặc chứng minh tự động tính đúng đắn của hàm sau từng lệnh.
Cho hàm f với đặc tả và cài đặt tương ứng :
Domain : P(x)
Where: Q(x, y)
Y f(X)
{
lệnh 1;
lệnh 2;
…
lệnh k;
}
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)
IV.2 CHỨNG MINH VỚI CÁC LUẬT SUY DIỄN
IV.2.1 Mở đầu
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 :
hay
Nếu và thì ta ký hiệu :
IV.2.2 Các luật suy diễn
IV.2.2.1 Các luật suy diễn trên phép phủ định (Ø)
(Ø-1)
IV.2.2.2 Các luật suy diễn trên phép hội (Ú)
a) Suy diễn mở rộng : Nếu đã có E rồi thì có thể suy diễn là có E hoặc là có bất cứ thứ gì khác nữa.
; (Ú-MR)
Ví dụ : Tôi đã có nhà. Vậy có thể nói "Tôi đã có nhà hoặc xe", hay "Tôi đã có xe hoặc nhà", bất kể là tôi đã thực sự có xe hay chưa.
b) Suy diễn theo trường hợp : Ta đã có E1 hoặc E2 (ít nhất 2 trong 2 thứ). Nếu từ E1 suy diễn ra được X, từ E2 cũng suy diễn ra được X. Như vậy ta suy diễn ra được X.
(Ú-TrH)
Ví dụ : Nếu đi làm thêm thì tôi sẽ có tiền.
Nếu được nhận học bổng thì tôi cũng sẽ có tiền
Mà hiện giờ tôi đã đi làm thêm hoặc đã nhận học bổng.
Vậy tôi có tiền.
c) De Morgan:
; (Ú-DM)
hay : (chiều thuận)
Ví dụ : Tôi không có xe hay nhà gì cả. Vậy tôi không có xe, mà cũng chẳng có nhà.
d) Tổng hợp trên phép hội:
(Ú-TH)
hay : (chiều đảo)
Ví dụ : Ngược lại, tôi không có xe, tôi cũng chẳng có nhà. Vậy tôi chẳng có xe hay nhà gì cả.
e) Thay thế trên phép hội:
; (Ú-TT)
f) Giao hoán trên phép hội:
(Ú-GH)
g) Kết hợp trên phép hội:
(Ú-KH)
h) Phân phối trên phép hội:
; (Ú-PP)
IV.2.2.3 Các luật suy diễn trên phép tuyển (Ù)
a)
và (Ù-1)
Ví dụ :Tôi đã có cả xe lẫn nhà. Vậy không thể có chuyện tôi không có xe hay không có nhà, và ngược lại.
b) Suy diễn thu hẹp (rút gọn) :
và (Ù-RG)
Ví dụ :Tôi đã có cả xe lẫn nhà. Vậy tôi có xe.
Tôi đã có cả xe lẫn nhà. Vậy tôi có nhà.
c) Tổng hợp trên phép tuyển :
(Ù-TH)
Ví dụ :Tôi đã có xe. Tôi cũng có nhà. Vậy tôi có cả xe lẫn nhà.
d) Thay thế trên phép tuyển :
; (Ù-TT)
Ví dụ :Tôi đã có cả xe lẫn nhà. Nếu có nhà thì tôi có đất. Vậy tôi có cả xe lẫn đất.
e) Phân phối trên phép tuyển :
; (Ù-PP)
IV.2.2.4 Các luật suy diễn trên phép kéo theo (Þ)
a) Suy diễn theo luật bài tam :
(BT)
b) Suy diễn dựa trên mẫu thuẫn :
(MT)
c) Suy diễn kéo theo :
; (Þ-1)
d) Suy diễn tương đương :
(Þ-2)
IV.2.3 Chứng minh luật suy diễn
IV.2.3.1 Dạng thức :
Để chứng minh luật suy diễn : , ta áp dụng dạng thức như sau :
From E
Kết quả 1 Luật suy diễn áp dụng(các kết quả sử dụng)
Kết quả 2 Luật suy diễn áp dụng(các kết quả sử dụng)
...
Infer F
IV.2.3.2 Ví dụ
Chứng minh lại các luật suy diễn sau :
1.
2.
3.
4.
Giải :
1. From (h)
1. Ù-1(h)
2. Ú-DM(1)
Infer E1 Ø-1(2)
2. From (h)
1. Ø-1(h)
2. Ú-TH(1)
Infer Ù-1(2)
3. From (h)
1. Ù-RG(h)
2. Ù-RG(h)
3. h(1)
Infer Ù-TH(1,3)
4. From (h)
1. From (h1)
Infer Ù-MR(h1)
2. From (h2)
2.1 h(h2)
Infer Ù-MR(2.1)
Infer Ù-TrH(h,1,2)
IV.3 BÀI TẬP ÁP DỤNG
Chứng minh các luật suy diễn sau :
1. (Ú-GH)
2. (Ú-KH)
3. ; (Ú-PP)
4. ; (Ù-PP)
5.
6.
7.
8.
9. ;
10. ;
11.
12.
13.
14.
15. ;
16.
17.
18.
19.
20. Tìm phản ví dụ để CM chiều nghịch là không đúng!
21.
22. ;
Bạn đang đọc truyện trên: AzTruyen.Top