Giáo trình Công nghệ phần mềm - Chương 6: Kiểm tra chất lượng phần mềm

ng được diễn tả dưới dạng có liên quan tới cấu trúc điều khiển 
của sự vật kiểm thử, và báo cáo về giá trị bao quát cho chuyên gia đảm bảo 
chất lượng.
 Dụng cụ kiểm thử. Lớp các công cụ này hỗ trợ cho việc xử lý các phép kiểm 
thử bằng cách làm gần như không khó khăn để (1) thiết lập một chương 
trình ứng cử viên trong môi trường kiểm thử, (2) nạp dữ liệu vào, và (3) mô 
phỏng bằng các cuống cho hành vi của các module phụ.
 Bộ so sánh cái ra. Công cụ này làm cho người ta có thể so sánh một tập cái 
ra từ một chương trình này với một tập cái ra khác (đã được lưu giữ trước) 
để xác định sự khác biệt giữa chúng.
 Hệ thống thực hiện ký hiệu. Công cụ này thực hiện việc kiểm thử chương 
trình bằng cách dùng cái vào đại số, thay vì giá trị dữ liệu số. Phần mềm 
được kiểm thử vậy xuất hiện để kiểm thử các lớp dữ liệu, thay vì chỉ là một 
trường hợp kiểm thử đặc biệt. Cái ra là đại số và có thể được so sánh với kết 
quả trông đợi cũng được xác định dưới dạng đại số.
 Bộ mô phỏng môi trường. Công cụ này là một hệ thống dựa trên máy tính 
giúp người kiểm thử mô hình hoá môi trường bên ngoài của phần mềm thời 
gian thực và rồi mô phỏng các điều kiện vận hành thực tại một cách động.
 Bộ phân tích luồng dữ liệu. Công cụ này theo dõi dấu vết luồng dữ liệu đi 
qua hệ thống (tương tự về nhiều khía cạnh với bộ phân tích đường đi) và cố 
gắng tìm ra những tham khảo dữ liệu không xác định, đặt chỉ số sai và các 
lỗi khác có liên quan tới dữ liệu.
Hiện nay việc dùng các công cụ tự động hoá cho kiểm thử phần mềm đang phát 
triển, và rất có thể là ứng dụng đó sẽ phát triển nhanh trong thập kỷ tới. Các công cụ 
kiểm thử có thể sẽ gây ra những thay đổi lớn trong cách chúng ta kiểm thử phần mềm 
và do đó cải tiến độ tin cậy của các hệ thống dựa trên máy tính.
6.4. CHỨNG MINH TOÁN HỌC TÍNH ĐÚNG ĐẮN CỦA CHƯƠNG TRÌNH 
Như đã đề cập ở trên, mục tiêu của chứng minh toán học là để có thể khẳng 
định tính đúng của chương trình thông qua chính văn bản của chương trình.
6.4.1. Khái niệm chung
Như ta đã biết, chương trình P là một bộ biến đổi tuần tự P để chuyển cái vào x 
thành ra cái y; ở đây x và y hoàn toàn được xác định trước.
Như vậy, một chương trình P được gọi là đúng nếu nó thực hiện chính xác 
những mục tiêu do người thiết kế đặc ra. Ta gọi:
+ Giả thiết A là mệnh đề được phát biểu để thể hiện tính chất của cái vào, gọi 
tắt là mệnh đề dữ liệu vào.
134
Chương 6: Kiểm tra chất lượng phần mềm
+ Kết luận B là mệnh đề được phát biểu để tính chất cần có của dữ liệu ra, 
gọi tắt là mệnh đề dữ liệu ra.
Do P có tính tuần tự và hữu hạn nên có thể biểu diễn P là một dãy liên tiếp các 
cấu trúc điều khiển P1, P2,....,Pn. Do vậy, bằng cách nào đó mà ta khẳng định được:
P1 biến đổi A thành A1
P2 biến đổi A1 thành A2
....
Pn biến đổi An-1 thành An
Và dựa vào quy tắc toán học, An có thể suy ra B thì ta có thể nói rằng P là 
đúng với cái vào A và cái ra B. Lúc này ký hiệu APB hay 
Cần chú ý rằng là khác với :mệnh đề {A} suy diễn ra mệnh đề 
{B} dựa vào các quy tắc toán học.
Nói cách khác, để chứng minh P là đúng, 
ta chứng minh theo sơ đồ sau:
A P1 A1
A1 P2 A2
.....
......
An-1PnAn
Ở đây, cần để ý là tính chất A và 
tính chất B có thể không liên quan đến nhau.
Ví dụ 1: Cho mệnh đề dữ liệu vào {A: x,y∈R; 0<x<1}
Đoạn trình P =P1∪P2∪P3∪P4 như sau:
x:=1/x+1; (P1)
y:=y+1; (P2)
x:=x+2; (P3)
x:=x+y; (P4)
và mệnh đề dữ liệu ra {B: x,y∈R; x>y+3}
Lúc này ta có dãy biến đổi tính chất dữ liệu vào/ ra như sau:
{A} P1{A1: x,y∈R; x>2}
{A1}P2{A2: x,y∈R; x>2}
{A2}P3{A3: x,y∈R; x>4}
{A3}P4{A4: x,y∈R; x>y+4}
và 
Vậy ta có kết luận {A}P{B} hay nói cách khác là P đúng với dữ liệu vào {A} 
và dữ liệu ra {B}.
135
P
1
P
2
P
n
A 
A
1
A
n
B
A=>B. P
A=>B P A=>B L
A
n=>B 
L
Ơ
A
4=>B 
L
Ơ
Chương 6: Kiểm tra chất lượng phần mềm
Cần để ý rằng khí ta có dãy biến đổi tính chất dữ liệu vào và ra như sau:
A P1 A1
A1 P2 A2
.....
......
An-1PnAn
Thì chưa thể kết luận được điều gì vì còn tuỳ thuộc vào các mệnh đề trung gian 
thu được {A1},{A2},....{An} là đã "mạnh nhất" hay chưa.
Xét ví dụ đã cho ở trên, ta có dãy biến đổi như sau:
{A} P1{A'1: x,y∈R; x>0}
{A'1}P2{A'2: x,y∈R; x>0}
{A'2}P3{A'3: x,y∈R; x>2}
{A'3}P4{A'4: x,y∈R; x>y+2}
Rõ ràng ta có: nhưng theo trên ta vẫn có kết luận {A}P{B}.
Trong trường hợp này, ta thấy các mệnh đề {A'1}{A'2}{A'3}{A'4} rõ ràng là các mệnh 
đề hệ quả của các mệnh đề {A1}{A2}{A3}{A4}.
Ví dụ 2: Cho mệnh đề dữ liệu vào {A: x,y∈N; x=3y}, đoạn trình P =P1∪P2 
như sau:
x:=x+5; (P1)
y:=y+5; (P2)
và mệnh đề dữ liệu ra {B: x,y∈R; x=3y}. Ở đây, rõ ràng ta có 
6.4.2. Hệ tiên đề Hoare
1. Tiên đề 1: Tiên đề tuần tự
Nếu mệnh đề A sau khi chịu tác động của khối cấu trúc điều khiển P ta được 
B và mệnh đề B sau khi chịu tác động của cấu trúc điều khiển Q ta được C thì 
A chịu tác động tuần tự P,Q sẽ thu được C
Hay nói cách khác, đây chính là tiên đề về dãy thao tác: Nếu A P B và B 
Q C thì A P,Q C
2. Tiên đề gán: tính chất của phép gán
Điều kiện để có mệnh đề B sau khi thực hiện lệnh gán x: = E (với E là một 
biểu thức) từ mệnh đề {A} thì trước đó ta phải có {A} suy dẫn được ra {B[x|E]}.
Mệnh đề {B[x|E]} là mệnh đề thu được từ {B} bằng phép thay thế mọi xuất 
hiện của x trong {B} bởi E. Tức là: A x: = E B thì 
136
A
n≠>B 
L
Ơ
A'
4≠>B L
A≠>B P
A=>B[x|E] L
Chương 6: Kiểm tra chất lượng phần mềm
 Kỹ thuật lần ngược của tiên đề gán
Cho đoạn trình P gồm n phép gán x1:=E1; x2:=E2;.......xn:=En; để {A}P{B} thì
ta phải có Trong đó {Bn} được xác định như sau
Trong đó các mệnh đề {Bi} được xác 
định như sau:
{B1} là mệnh đề {B[xn|En]}
{Bn-1} là mệnh đề {Bn-2[x2|E2]}
{Bn} là mệnh đề {Bn-1[x1|E1]}
Trong trường hợp thì ta nói P là có lỗi.
Ví dụ 3: (Xét ví dụ 1) Cho mệnh đề dữ liệu vào {A: x,y∈R; 0<x<1}, 
Đoạn trình P =P1∪P2∪P3∪P4 như sau:
x:=1/x+1; (P1)
y:=y+1; (P2)
x:=x+2; (P3)
x:=x+y; (P4)
và mệnh đề dữ liệu ra {B: x,y∈R; x>y+3}. Hãy khảo sát {A}P{B} hay không?
Ta có
{B[x|x+y]} ≡{B1 : x+y,y∈R; x+y>y+3}
{B1[x|x+2]} ≡{B2 : (x+2)+y,y∈R; (x+2)+y>y+3}
{B2[y|y+1]} ≡{B3 : (x+2)+(y+1),(y+1)∈R; (x+2)+(y+1)>(y+1)+3}
{B3[x|1/x+1]} ≡{B4 : ((1/x+1)+2)+(y+1),(y+1)∈R; ((1/x+1)+2)+(y+1)>(y+1)+3}
Rõ ràng ta có , nên {A}P{B}.
137
A=>B
n.
L
B
n-1
B
n
x
1
:=E
1
x
2
:=E
2
x
n
:=E
n
A 
B
1
B
A=>B
4. 
L
A≠>B
n 
L
Chương 6: Kiểm tra chất lượng phần mềm
3. Tiên đề rẽ nhánh
i. Với mệnh đề dữ liệu vào {A}, mệnh đề dữ liệu ra {B}, biểu thức logic E, 
và đoạn trình P. Nếu ta có {A, E}P{B} và thì ta nói rằng mệnh đề {A} 
và {B} tuân theo cấu trúc rẽ nhánh dạng khuyết với cấu trúc P và điều kiện lựa chọn E; 
tức là: {A} if E then P; {B}.
ii. Với mệnh đề dữ liệu vào {A}, mệnh đề dữ liệu ra {B}, biểu thức logic E, 
và các đoạn trình P, Q. Nếu ta có {A, E}P{B} và {A,!E}Q{B} thì ta nói rằng mệnh đề 
{A} và {B} tuân theo cấu trúc rẽ nhánh dạng đủ với cấu trúc P, Q và điều kiện lựa 
chọn E; tức là: {A} if E then P else Q; {B}.
Ví dụ 4: Cho mệnh đề dữ liệu vào {A: x,y,q,r∈N, x=qy+r, 0≤r<2y}, đoạn trình 
P như sau:
If y≤r then 
Begin
q:=q+1;
r:=r-y;
End;
Và mệnh đề dữ liệu ra {B: x,y,q,r∈N, x=qy+r, 0≤r<y}. Hãy xem {A}P{B}? 
Áp dụng tính chất của phép gán, ta có:
i. {A,E: x,y,q,r∈N, x=qy+r, 0≤ r<2y, y≤ r}q:=q+1;r:=r-y;{B}
ii. {A,!E: x,y,q,r∈N, x=qy+r, 0≤ rr}=>{B}
do đó suy ra {A}P{B}.
4. Tính bất biến của chương trình 
Cho mệnh đề dữ liệu vào {A} và đoạn trình P. Nếu ta có {A}P{A} thì ta nói 
rằng tính chất dữ liệu của mệnh đề {A} không thay đổi khi chịu sự tác động của đoạn 
trình P và lúc này người ta nói rằng mệnh đề {A} là bất biến đối với P, tức ta có: {A}P 
{A}.
Ví dụ 5: Ta có mệnh đề {A: x∈R, x>0} là bất biến đối với đoạn trình P: x:=x*x; 
vì ta có {A}P{A}.
5. Tiên đề lặp
Cho mệnh đề dữ liệu vào {A}, biểu thức logic E và đoạn trình P. Nếu mệnh đề 
{A} tuân theo cấu trúc lặp P với điều kiện lặp E thì mệnh đề {A} sẽ bất biến đối với P 
trong điều kiện E, tức là {A,E}P{A}, kết thúc vòng lặp ta có mệnh đề {A,!E}. Lúc này 
ta viết: {A} while E do P; {A,!E}.
138
A,!E=>BL
L
Chương 6: Kiểm tra chất lượng phần mềm
Ví dụ 6: Cho x,y,z là 3 số nguyên không âm. Hãy viết chương trình để tính 
z=xy, biết rằng x,y được nhập từ bàn phím. Hãy khẳng định tính đúng của chương 
trình.
Ta có đoạn trình như sau:
Vào: x,y,z∈N; x=a; y=b;
Ra: x,y,z∈N; z=ab;
Chương trình P được viết:
z:=0;
while x>0 do
Begin
 If (x mod 2)≠0 then z:=z+y;
x=x div 2;
y:=y*2;
End;
Return z;
Ta cần phải khẳng định chương trình trên đúng với yêu cầu đặt ra.
Thật vậy, gọi mệnh đề thể hiện tính chất dữ liệu vào của chương trình {A} và 
mệnh đề thể hiện tính chất dữ liệu ra cần có {B}, ta có
{A: x,y,z∈N; x=a; y=b;} và {B: x,y,z∈N; z=ab;}
Ta cần chứng tỏ {A}P {B}.
+ Xét mệnh đề {C: x,y,z∈N; ab=z+xy;}
+ Ta có {A} z:=0;{C}
+ Để chứng tỏ {C} là bất biến của đoạn trình
while x>0 do
Begin
 If (x mod 2)≠0 then z:=z+y;
x=x div 2;
y:=y*2;
End;
Ta cần có: {C,E: x,y,z∈N; ab=z+xy;x>0}Q{C}, với đoạn trình Q như sau:
If (x mod 2)=0 then z:=z+y;
x=x div 2;
y:=y*2;
Theo tính chất của phép gán, ta có:
{C1}≡{C[y|y*2]: x,y*2,z∈N; ab=z+x(y*2);}
{C2}≡{C1[x|(x div 2)]: (x div 2),y*2,z∈N; ab=z+(x div 2)(y*2);}
Nên cần chứng tỏ:
{C,E: x,y,z∈N; ab=z+xy;x>0} If (x mod 2)≠0 then z:=z+y; {C2}
Dễ dàng ta có
i. {C,E,F: x,y,z∈N; ab=z+xy;x>0,(x mod 2)≠0} z:=z+y {C2}; và
ii..{C,E,!F: x,y,z∈N; ab=z+xy;x>0,(x mod 2)=0} =>{C2}; 
139
L
Chương 6: Kiểm tra chất lượng phần mềm
Vậy {C} là bất biến của Q. Nên kết thúc Q, ta có mệnh đề {C,!E}.
+ Dễ dàng chứng tỏ: {C,!E}=>{B} 
Vậy ta có {A}P{B}, hay chương trình trên là đúng.
Để ý rằng: do {A,E}P{A} nên trong trường hợp {A}=>E thì vòng lặp là vô 
hạn và không tồn tại mệnh đề {A, !E}.
140
L
L