Giáo trình Mô đun Công nghệ phần mềm - Lập trình máy tính

m, nếu chỉ có black-box các vấn đề logic đặc trưng có thể chưa được khám phá.
5.3. Kỹ thuật kiểm thử phần mềm và đặc điểm
5.3.1. Khái niệm
Kiểm thử một sản phẩm phần mềm là xây dựng một cách có chủ đích những tập dữ liệu và dãy thao tác nhằm đánh giá một số hoặc toàn bộ các tiêu chuẩn của sản phẩm phần mềm đó.
Thử nghiệm có hai mục đích: chỉ ra hệ thống phù hợp với đặc tả và phơi ra được các khuyết tật của hệ thống.
5.3.2. Đặc điểm của kiểm thử
Các hạn chế của kiểm thử
Do kiểm thử là chạy thử chương trình với tập dữ liệu giả nên không thể khẳng định tính đúng của chương trình do bản chất quy nạp không hoàn toàn của nó.
Trong nhiều trường hợp, việc kiểm thử thường được thực hiện từ những giai đoạn đầu của quá trình cài đặt sản phẩm.
Các chương trình nên được kiểm chứng theo hai kỹ thuật: kiểm thử và chứng minh. Và nếu có thể nên khẳng định tính đúng của chương trình thông qua văn bản chương trình
Như vây, một chương trình tuyệt đối đúng phải được thực hiện thông qua: tính đúng đắn của thuật toán và tính tương đương của chương trình với thuật toán (được thể hiện ở chứng minh thông qua văn bản chương trình). 
Việc kiểm thử chương trình chỉ là nhìn sự kiện đưa ra kết luận do vậy không thể khẳng định một chương trình tuyệt đối đúng bằng kiểm thử. Tuy vậy, bộ dữ liệu kiểm thử phải phủ kín mọi trường hợp cần đánh giá.
Thêm vào đó, trong quá trình kiểm thử, ta thưòng mắc phải các đặc trưng của nguyên lý chủ quan như sau:
Bộ dữ liệu Test không thay đổi trong quá trình xây dựng phần mềm 
Chỉ Test các trường hợp chính thống, hợp lệ, không quan tâm đến các cận và các sự cố
Cài đặt chức năng nào thì chỉ Test riêng chức năng đó, không chỉ Test tổng hợp chức năng vừa cài đặt với các chức năng đã cài đặt trước đó.
Người Test đồng thời là người xây dựng phần mềm tức vừa đá bóng, vừa thổi còi.
Các loại hình kiểm thử
Kiểm thử lược đồ hệ thống: chỉ quan tâm đến các bản chọn (menu) đánh giá tính hợp lý, khả năng chọn một mục, khả năng di chuyển qua mục khác, tính đủ, tính khoa học của các chức năng.
Kiểm thử cận dưới
Kiểm thử cận trên: cho hệ thống thực hiện đến mức tối hạn.
Kiểm thử qua sự cố: tạo ra các sự cố để kiểm thử phần mềm.
Nguyên tắc kiểm thử
Nguyên tắc khách quan: người kiểm thử không phải là tác giả của phần mềm đang kiểm thử
Nguyên tắc ngẫu nhiên: dữ liệu và chức năng được chọn, tuy có chủ đích nhưng không phải xuất hiện theo thứ tự nhất định.
Nguyên tắc "người sử dụng kém": hệ thống được một người sử dụng có trình độ thấp (ở mức chấp nhận được) dùng thử. (Người này có thể gây các sự cố có thể không lường trước được của hệ thống )
Nguyên tắc "kẻ phá hoại": hệ thống rơi vào tay có trình độ nghiệp vụ cao, chủ ý phá hoại. "Trình độ" ở đây thuộc lĩnh vực công nghệ thông tin hoặc lĩnh vực phần mềm đang hướng tới.
Kỹ thuật kiểm thử
Kỹ thuật đối xứng: dựa vào tính đối xứng của các thao tác hoặc tập dữ liệu để xậy dựng bộ dữ liệu Test.
Kỹ thuật đám đông
Kỹ thuật kiểm thử trên dữ liệu thật: cho hệ thống vận hành với các tập dữ liệu thật đã thu được từ trước để so sánh và đánh giá kết quả
Kỹ thuật kiểm thử trên thị trường thật: cho hệ thống vận hành trên thị trường thật (không chính thức) để so sánh với các hệ thống chính được dùng và đánh giá kết quả.
Kỹ thuật đối sánh: cho thực hiện với một vài sản phẩm khác với cùng các chức năng giống nhau và trên cùng các tập dữ liệu rồi lập bảng so sánh các chức năng.
Quá trình kiểm thử
Trừ hệ thống nhỏ, nói chung không nên kiểm thử nguyên cả khối; quá trình kiểm thử có thể chia 5 giai đoạn:
Thử đơn vị
Thử module
Thử hệ con
Thử hệ thống
Thử nghiệm thu: còn gọi thử anpha.
Khi hệ thống được đem bán còn phép thử beta: phân phối hệ thống cho một số người dùng đồng ý dùng thử và báo cáo lại các vấn đề cho người phát triển hệ thống.
5.3.3. Kế hoạch thử nghiệm
Thử hệ thống là rất đắt đỏ, đối với một vài hệ thời gian thực có các ràng buộc thời gian phức tạp thì việc thử có thể ngốn hết khoảng nửa tổng chi phí phát triển.Vì thế mà phải lập kế hoạch thử và khống chế chi phí thử. 
Cần chú ý là việc thử liên quan đến việc thiết lập ra các mẫu cho quá trình thử nhiều hơn là mô tả các phép thử.
6.3.4. Phân loại một số công cụ kiểm thử tự động
	Vì kiểm thử phần mềm thường chiếm tới 40% tất cả các nổ lực dành cho một dự án xây dựng phần mềm, nên công cụ có thể làm giảm thời gian kiểm thử (không làm giảm tính kỹ lưỡng) sẽ rất có giá trị. Thừa nhận lợi ích tiềm năng này, các nhà nghiên cứu và người thực hành đã phát triểnmột số thế hệ các công cụ kiểm thử tự động:
Bộ phân tích tĩnh. Các hệ thống phân tích chương trình này hỗ trợ cho "việc chứng minh" các lý lẽ tĩnh - những mệnh đề yếu kém về cấu trúc và định dạng của chương trình.
Bộ kiểm toán mã. Những bộ lọc chuyên dụng này được dùng để kiểm tra chất lượng của phần mềm để đảm bảo rằng nó đáp ứng các chuẩn mã hoá tối thiểu.
Bộ xử lý khẳng định. Những hệ thống tiền xử lý/hậu xử lý này được sử dụng để cho biết liệu những phát biểu do người lập trình nêu, được gọi là các khẳng định, về hành vi của chương trình có thực sự được đáp ứng trong việc thực hiện chương trình thực hay không.
Bộ sinh tệp kiểm thử. Những bộ xử lý này sinh ra, và điền các giá trị đã xác định, vào các tệp đọc vào điển hình cho chương trình đang được kiểm thử.
Bộ sinh dữ liệu kiểm thử. Những hệ thống phân tích tự động này hỗ trợ cho người dùng trong việc chọn dữ liệu kiểm thử làm cho chương trình hành xử theo một cách đặc biệt.
Bộ kiểm chứng kiểm thử. Những công cụ này đo mức bao quát kiểm thử bên trong, thườ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.
5.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.
5.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.
+ 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ý
íAý=>íBý 
LƠ
íAý=>íBý là
PƠ
íAý=>íBý. 
PƠ
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ý=>íBý 
LƠ
í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}
íA4ý=>íBý 
LƠ
{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}.
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ý¹>íBý 
LƠ
í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'4ý¹>íBý 
 L
{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)
íAý¹>íBý 
P
y:=y+5;	(P2)
và mệnh đề dữ liệu ra {B: x,yÎR; x=3y}. Ở đây, rõ ràng ta có 
5.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]}.
íAý=>íB[x|E]ý 
L
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ì 
Kỹ thuật lần ngược của tiên đề gán
íAý=>íBný. 
L
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]}
íAý¹>íBný 
L
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}
íAý=>íB4ý. 
L
{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}.
3. Tiên đề rẽ nhánh
íA,!Eý=>íBý
L
	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}
L
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}.
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}.
	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à
L
ii..{C,E,!F: x,y,zÎN; ab=z+xy;x>0,(x mod 2)=0} =>{C2}; 
L
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.
L
	Để ý 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}.