Cho W là một lệnh lặp while B do S và cặp đkđ P, đkc Q.
Ta cần phải chứng minh rằng : đặc tả { P } W { Q } được thỏa đầy đủ . Để chứng minh W thoả đầy đủ đặc tả P,Q ta cần chỉ ra 2 điều :
(i) P bảo đảm W dừng,tức là xuất phát từ trạng thái bất kỳ thoả P,thì hành W thì W sẽ dừng sau một thời gian hữu hạn ( sau khi thực hiện hưu hạn lần lệnh S ở thân vòng lặp W thì B sẻ có gía trị false ).
(ii) {P} W {Q} - Đúng có điều kiện ( xuất phát từ trạng thái thỏa P sau khi thi hành W nếu W dừng thì sẻ đạt tới trạng thái thỏa Q ).
Để chứng minh (ii) ta có thể dùng hệ ; luật Hoare mà chủ yếu là phải phát hiện được bất biến I.
Để chứng minh (i) W dừng ta cần dựa trên các biến bị thay đổi trong vòng lặp thường dựa vào một hàm f của các biến chương trình nhận gía tri nguyên và chỉ ra rằng :
(α) Ở đầu mỗi lần lặp ( B thoả ) thì f > 0 .
(β) Mỗi lần thực hiện S sẽ làm giảm thực sự giá trị của f.
Nếu (α) và (β) thoả thì S không thể lặp vô tận được (vì sau hưu hạn lần thì B sẻ nhận gía trị false ).
Xét đặc tả đoạn chương trình tính tích 2 số nguyên A và B với B >= 0 bằng phép cộng :
{ B >= 0 } R := 0 ;
X := B ;
while (X <>0 ) do begin
R := R + A ;
X := X - 1 ; end ;
{ R = A*B }
đkđ P ≡ B >= 0
đkc Q ≡ R = A * B
Bước 1: Kiểm chứng tính đúng có điều kiện của đặc tả {P} S {Q}
+ Kiểm chứng đoạn lệnh trước vòng lặp : Chứng minh đặc tả sau đúng .
{ B >= 0 }
R := 0 ; (*)
X := B ;
{X = B , R = 0, B >= 0 }
Ta có :
{0 = 0 , B >= 0} R := 0 {R = 0 , B >= 0} (1) tiên đề gán
{0 = 0 , B >= 0} ⇒ { B >= 0} (2) hiển nhiên
{B >= 0} R := 0 {R = 0, B >= 0} (3) luật hệ quả dựa vào (1),(2)
{B = B , R = 0 , B >= 0} X := B {X = B , R = 0 , B >= 0} (4) tiên đề gán
{B =B , R =0 , B >= 0} ⇒ { R = 0 , B >= 0 } (5) hiển nhiên
{R = 0 , B >= 0} X := B {X := B , R = 0 , B >= 0} (6) Luật hệ quả dựa vào
(4),(5)
{B >= 0} X := 0 ; X :=B {X = B , R = 0 , B >= 0} (7) luật tuần tự dựa vào (3),(6).
Như vậy với điều kiện đầu B >= 0 thì sau khi thực hiện xong 2 lệnh khởi động, ta có khẳng định X = B, R = 0, B >= 0 đặc tả (*) đúng .
+ Kiểm chứng vòng lặp :
- Phát hiện được bất biến của vòng lặp.
Bất biến ở đây là : “ số lần X bị giảm đi chính là số lần A được cộng vào R “ Tức là : I ≡ ( R = A*(B-X) ) and ( X >= 0 )
Khẳng định (X >= 0 ) được thêm vào để chứng minh vòng lặp dừng. - Chứng minh I là bất biến của vòng lặp :
{( R + A = A*B - A*X + A ) and ( X >0 )} R := R + A
{(R = A*B - A*X + A ) and ( X > 0 )} (8) tiên đề gán
{ ( R = A*(B - X)) and ( X > 0 )}
R := R + A
{ ( R = A*B - A*X + A ) and ( X > 0 )} (9) biến đổi từ (8)
{ ( R = A*B - A*X + A ) and ( X > 0 )} ≡ { ( R = A*(B -(X - 1)) ) and ( (X - 1 ) >= 0 )}(10)
{ ( R = A*(B -(X - 1)) ) and (( X - 1 ) >= 0 )}
X := X - 1
{( R = A*(B - X)) and ( X>=0 ) }
{( R = A*B - A*X + A) and (X > 0)}
X := X - 1
{( R = A*(B - X ) ) and ( X >= 0 )} {(R = A*(B -X )) and ( X > 0 )}
R : = R+A ; X := X - 1
{( R = A*(B - X )) and ( X >= 0 )}
(11) tiên đề gán
(12) luật hệ quả
(13) luật tuần tự dựa vào (9 ),(12)
{(R = A*(B - X )) and (X >= 0 ) and (X<>0)} ==> {(R =A*(B - X )) and (X >0 )}(14)
{(R = A*(B - X )) and (X >= 0) and (X<>0)}
R := R+A ; X := X-1
{(R = A*(B - X )) and (X >= 0)} (15) luật hệ quả dựa vào (13 ),(14)
Hay {I and C} R := R + A ; X := X - 1 {I}
với C là điều kiện vòng lặp X<>0
Do luật lặp ta có :
{I} while ... {I and not C}
(X=B) and (R=0) and (B>=0) ==> (R=A*(B-X)) and (X>=0) (16) Kết hợp 15,16 và 5 dùng luật hệ quả rồi luật tuần tự, ta có : {X=B and R=0 and B>=0} while ... {I and notC} (17) {B>=0} R:=0 ; X:=B ; while ... {I and notC} (18) Ở đây I and not C ≡ ( R = A*(B-X)) and (X >= 0 ) and (X = 0)
mà ( R = A*(B-X)) and ( X >= 0) and (X=0) ==> R=A*B Dùng luật hệ quả ta có đpcm
Bước 2 : Chứng minh tính dừng : Đặt f = X, ta có :
(i) I and C ≡ ( R = A*(B-X) ) and ( X >= 0) and (X<>0 ) => X > 0 => f > 0
(ii) Mỗi lần lặp, f bị giảm một đơn vị. Vậy vòng lặp phải dừng.
Từ (i) và (ii) ta kết luận được tính dừng từ bước 1 và bước 2 suy ra tính đúng đầy đủ của đoạn chương trình đối với P,Q.
Nhận xét từ chứng minh trên :
+ Đối với dãy các lệnh gán, nên phát xuất quá trình suy diễn từ điều kiện cuối. + Đối với vòng lặp cần xác định đúng bất biến của nó.
Chú ý : Ta có thể kiểm chứng tđcđk của đoạn chương trình trên bằng cách:
- Xây dưng một lư?c đồ chứng minh hợp lý bằng cách dựa vào các tiên đề và càc khẳng định đã có trước đó chèn bổ sung các khẳng định trung gian ở những điểm khác nhau trong đoạn chương trình .
{P } ≡ { B >= 0 } (0)
{(0 = A*(B - B )) and (B >= 0 )} (3)
R := 0 ;
{(R = A*(B - B )) and (B >= 0)} (2)
X := B ;
{I } ≡ {( R = A*(B - B )) and ( X >= 0 )} (1a)
while (X <>0 ) do begin
{I and C } ≡ {( R = A*(B - X )) and (X >= 0) and (X<>0)} (1b)
{(R + A = A*(B -(X - 1 )) and ( (X -1 ) >= 0)} (5)
R := R+A ;
{( R = A*(B -(X - 1 )) and ( (X - 1 ) >= 0)} (4)
X := X - 1 ;
{I } ≡ {(R = A*(B - X)) and ( X >= 0 )} (1d)
end
{I and notC } ≡ {( R = A*(B - X ) ) and (X >= 0) and not(X <> 0)} (1c)
{Q } ≡ { R = A*B} (6)
Lý lẽ để bổ sung là :
(1a) do phát hiện được bất biến I
(1b),(1c),(1d) dựa vào tiên đề về lệnh lặp xuất phát từ I 2, 3 dựa vào tiên đề gán xuất phát từ (1a)
4, 5 dựa vào tiên đề gán xuất phát từ (1d)
Các cặp khẳng định đi liền nhau là các điều kiện cần kiểm chứng :
(0) ==> (3) : ( B >= 0 ) ==>( (0 = A * (B-B)) and (B >= 0 ) )
(1b) ==> (5) : (( R = A*(B - X )) and (X >= 0) and (X<>0)) ==>
((R + A = A*(B -(X - 1 )) and ( (X -1 )
>= 0))
(1c) ==> (6) : ( (R = A*(B-X)) and (X >= 0) and (X = 0)) ==> ( R=A*B )
Dễ dàng chứng minh các điều trên.
