Kiểm chứng tính đúng có điều kiện

Kiểm chứng tđcđk đặc tả sau :

{ x = 3 } x := 5 ; y := 2 { x = 5, y = 2 }

Ta có : { true} x := 5 ; y := 2 { x = 5 ; y = 2 } (a) // tạm công nhận

và ( x = 3 ) => true (b) // hiển nhiên

Nên { x = 3 } x := 5 ; y := 2

Kiểm chứng tđcđk đặc tả sau :

{ x > 3 } x := x -1 { x > 0 }

Ta có : { x > 1 } x := x-1 { x > 0 }

và ( x > 3 ) => ( x > 1)

{ x = 5, y = 2 } // theo tiên đề (1a)

(a) //tạm công nhận

(b) // hiển nhiên

Nên { x > 3 } x := x -1 { x > 0 } // theo tiên đề (1a)

b)

Kiểm chứng tđcđk đặc tả sau :

{ true } x := 5 ; y := 2 { odd(x) and even(y) }

Ta có : { true } x := 5 ; y := 2 { (x = 5) , ( y = 2 ) } (a) // tạm công nhận

và ( (x = 5) and (y = 2)) => odd(x) and even(y) (b) // hiển nhiên

Nên { true } x := 5 ; y := 2 { odd(x) and even(y) } //theo (1b)

Kiểm chứng tđcđk đặc tả :

{ x > 1 } x := x -1 { x >= 1 }

Ta có : { x > 1 } x := x-1 { x > 0 } (a) // tạm công nhận

và ( x > 0 ) => ( x >= 1) // (b) // vì x là biến nguyên

Nên { x > 1 } x := x -1 { x >= 1 } // theo (1b)

Hai luật này cho phép liên kết các tính chất phát sinh từ cấu trúc chương trình với các suy diễn logic trên dữ kiện.

Kiểm chứng tính đúng của đoạn lệnh hoán đổi nội dung 2 biến x và y

a) {(x=x_o) and ( y = y_o ) }

t := x ; x := y ; y := t ;

{(x=y_o ) and (y = x_o ) }

Chứng minh

{(x = y_o ) and ( t = x_o) } y := t {(x = y_o ) and ( y = x_o ) } (a) // tiên đề gán

{(y = y_o ) and ( t = x_o ) } x := y {(x = y_o ) and ( t = x_o ) } (b ) // tiên đề gán

{(y = y_o ) and ( t = x_o ) } x := y ; y := t {(x = y_o) and ( y = x_o ) } (c) // a , b , luật

tuần tự {(y = y_o ) and ( x = x_o ) } t := x {(y = y_o ) and ( t = x_o ) } (d) // tiên đề gán

( (x = x_o ) and (y = y_o ) ) ≡ ( ( y = y_o ) and ( x = x_o ) } (e ) // giao hoán

{( x = x_o ) and (y = y_o ) } t := x {(y = y_o ) and ( t = x_o ) } (g) // d ,e, luật hệ quả

{(x = x_o ) and ( y = y_o ) } t := x ; x := y ; y := t {(x = y_o ) and ( y = x_o ) (h) // c ,g , luật tuần tự

Ví dụ1 : Kiểm chứng tính đúng của đặc tả : { (m :: k=2*m) and (y * z^k = c)} k := k div 2 ;

z := z * z ;

{ y * z^k = c} Chứng minh :

(a) {y * (z*z)^k = c} z := z * z {y*z^k = c} (tiên đề gán)

(b) {y * (z*z)^{k div 2} = c} k := k div 2 {y*(z*z)^k = c} (tiên đề gán)

(c) {y * (z*z)^{k div 2} = c} k := k div 2 ; z := z*z {y*z)^k = c} (a ,b , luật tuần tự)

(d) (m :: k = 2*m) and ( y * z^k = c ) ==> (y*z^2m = c) and ( m = k div 2 )

==> y * (z*z)^{k div 2} = c

c ,d , luật hệ quả suy ra ĐPCM.

Kiểm chứng đặc tả :

{ y > 0 }

x := y - 1 ;

if ( y > 3 ) then x := x * x else y := y - 1 ;

{ x >= y }

Trong ví dụ này :

P là tân từ : ( y > 0 ) ; Q là tân từ : ( x >= y )

B là biểu thức boolean : ( y > 3 )

S₀ là lệnh gán : x := y - 1 ;

Do S₁ và S₂ là lệnh gán : x := x * x ; S₂ là lệnh gán : y := y - 1 ;

Ta có :

{x² >= y} x := x*x {x >= y} suy ra U ≡ WP( S₁ , Q ) ≡ x 2 >= y

(a)

{x >= y-1} y := y-1 {x >= y} suy ra V ≡ WP( S₂ , Q ) ≡ x >= y-1

(b)

Đặt R ≡ (B ==> U) and (not B ==> V)

≡ ((y > 3) ==> (x² >= y)) and ((y <= 3) ==> (x >= y-1))

Ta chứng minh được dễ dàng.

R and (y>3) ==> (x² >= y)

R and (not(y>3)) ==> (x >= y-1)

nên theo luật hệ quả {R and y>3} S₂ {x >= y} (

{R and not(y>3)} S₃ {x >= y}

Theo luật về lệnh chọn

(c)

(d)

{R and B} S₂ {Q} ) (e)

( {R and (not B)} S₃ {Q} ) (g)

{R} if ( y>3) then x := x*x else y := y-1 {x >=y} (h)

theo tiên đề gán.

{ ((y>3) ==> ((y-1) 2 >=y)) and ((y <=3) ==> ((y-1) >= (y-1))) }

x := y -1

{ R } (i)

Dễ kiểm chứng được

(y>3) ==> ((y-1) 2 >= y ≡ true (j)

(y<=3) ==> (y-1) >= y-1 ≡ true (k)

nên

(y >0) ==> ((y>3) ==>((y-1)² >=y)) and ((y<=3) ==> ((y-1) >=(y-1))) (l) Theo luật hệ quả

{y > 0}

x := y-1;

if (y>3) then x := x*x else y := y-1

{ x >= y} (m) // ĐPCM

Kiểm chứng đặctả : { true }

if ( i <= j) then if (j<k ) then m := k else m := j

else if( i<k) then m := k else m := i {(m >= i) and (m >= j) and (m >= k)}

Đặt Q(m) ≡ ( m >= i) and (m >= j) and (m >= k)

Ta có :

(a) {Q(i)} m := i {Q(m)} (tiên đề gán)

(b) {Q(k)} m := k {Q(m)} (tiên đề gán)

Đặt R1 ≡ ((i < k) ==> Q(k)) and ( (i >= k) ==>Q(i))

dùng luật về lệnh chọn ta sẽ chứng minh được :

{R1} if ( i < k) then ... {Q(m)} (c)

Tương tự đặt R2 ≡ ( j<k) ==> ( Q(k) and (j >= k)) ==> Q(j)

Ta có: {R2} if (j < k ) then ... {Q(m)} (d)

Dùng biến đổi đại số và logic để chứng minh ( true and ( i <= j)) ==> R2 (e)

( true and ( i > j )) ==> R1 (g)

Từ c , d, e ,g , theo luật về lệnh chọn ta có ĐPCM. Nhận xét :

Để chứng minh đặc tả {P} S {Q} với S là tổ hợp lệnh gồm chỉ các lệnh gán và điều

kiện đúng đầy đủ ,ta thực hiện công việc xây dựng điều kiện đầu yếu nhất P₁ của S ứng với Q , sau đó bước kiểm chứng cuối cùng chỉ đơn giản là chứng minh : P ==> P₁. Công việc trên được trình bày dư?i dạng một hàm đệ quy như sau :

function DKDYN (S : nhóm_lệnh ; Q : tân_từ ) : tân_từ ;

var t : câu lệnh ;

begin

if (S <> rỗng ) then begin

t := lệnh_cuối(S);

S := S - t ;

if ( t = lệnh_gán(x:=bt)) then DKDYN := DKDYN(S,Q(

x=bt) )

else (* t là lệnh if *)

DKDYN := (điều_kiện(t)==>DKDYN(phần_đúng(t),Q))

and not (điều_kiện(t)==>DKDYN(phần_khong đúng(t),Q))

end

else DKDYN := Q

end ;

Với vòng lặp :

tg := 0 ;

i := 0 ;

while ( i <= n ) do begin

i := i + 1 ;

tg := tg + a[i] ; end ;

Từ các quan sát : 1 = 1 = 1²

1 + 3 = 4 = 2²

1 + 3 + 5 = 9 = 3²

1 + 3 + 5 + 7 = 16 = 4²

Bằng quy nạp người ta đặt giả thuyết : 1 + 3 + ... (2*n - 1) = n²

Ta có thể thử lại giả thuyết này với n = 5, 6... . Tuy nhiên, để khẳng định rằng giả thuyết đúng với mọi n, ta cần có chứng minh. Phưong pháp chứng minh thường dùng trong trường hợp này là chứng minh bằng quy nạp.

(i) Cơ sở : P(1) chính là 1 = 1² đúng

(ii) Giả sử P(n) đúng, tức là 1 + 3 + ... (2*m - 1) = n²

thì ta sẽ có :

1 + 3 + .... + ( 2*(n+1)-1 ) = (1+3+....+(2*n -1)) + (2*(n+1)-1)

= n² + 2*(n+1) - 1

= (n+1)²

Vậy P(n+1) đúng .Dựa vào (i) và (ii), ta kết luận P(n) đúng với mọi số tự nhiên n >=1 theo nguyên ly quy nạp toán học.

Chỉ ra các vòng lặp sau đây dừng : {n >= 0}

k := n ;

while (k <>0 ) do begin {k > 0} k := k-1 ;

r := 2*r + p[k];

if (r >= q) then r := r - q

end ;

vì bất biến {k > 0} luôn được giữ đúng ở đầu vòng lặp. Ở đây hàm f chính là

bằng k. f giảm sau mỗi lần lặp ( vì k := k - 1 ). Vậy vòng lặp dừng .

{x >= 0 ; y >= 0}

a := x ; b := y ;

while (a <>b) do

{max(a,b) > 0}

if (a>b ) then a := a - b else b := b - a

Ở đây hàm f = max(a,b). Ta luôn có bất biến max(a,b) > 0 ở đầu vòng lặp, f giảm sau mỗi lần lặp.

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: 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.