Kiểm chứng tính đúng đầy đủ
Đặt vấn đề. Ta thường gặp bài toán sau : Với tân từ Q trên các biến chương trình mô tả trạng thái cuối cần thỏa sau khi thực hiện lệnh S, tìm tập điêu kiện đầu thỏa đặc tả . Tức là với tân từ Q và đoạn lệnh S cho trước tìm ...
Đặt vấn đề.
Ta thường gặp bài toán sau : Với tân từ Q trên các biến chương trình mô tả trạng thái cuối cần thỏa sau khi thực hiện lệnh S, tìm tập điêu kiện đầu thỏa đặc tả . Tức là với tân từ Q và đoạn lệnh S cho trước tìm tân từ P thỏa đầy đủ đặc tả : {P} S {Q}.
Dễ thấy rằng bài tóan sẻ có nhiều lời giải. Xuất phát từ một cặp gồm tân từ Q và đoạn lệnh S , có nhiều tân từ P thỏa .
Với Q ≡ ( x > 0 ) ; S ≡ x := x - 1 ;
Các tân từ P sau đây đều thỏa :
(x > 1) , (x >= 5), (x > 5), ... , false
Mỗi tân từ P xác định một tập hợp các trạng thái. Trên tập hợp các trạng thái ứng cử này dĩ nhiên ta sẽ mong muốn chọn tập hợp lớn nhất có thể. Tức là ta quan tâm đến tân từ P là hạn chế yếu nhất trên không gian trạng thái . Dễ dàng thấy rằng ý nghĩa của quan hệ yếu ở đây là :
P yếu hơn Q tức là ( Q ==> P )
hoặc { Q } ⊆ { P }
Định nghĩa WP(S,Q).
Nếu Q là một tân từ trên các biến chương trình và S là một đoạn lệnh thì điều kiện đầu yếu nhất của S dựa trên Q (the weakest precondition of S with respect to Q ) là một tân từ trên các biến chương trình mô tả tập hợp mọi trạng thái ban đầu sao cho việc thi hành S bắt đầu ở một trạng thái thỏa nó đều được bảo đảm là sẽ dừng trong một trạng thái thoả tân từ cuối Q ( thuộc tập {Q} ),và được ký hiệu là WP(S ,Q )
Khái niệm WP là cơ sở cho việc mô tả một hệ thống quy tắc kiểm chứng tính đúng đầy đủ đoạn chương trình của Dijkstra . Ta sẽ tìm hiểu nôi dung của hệ thống này trong mối tương quan với hệ luật của Hoare.
Việc kết hợp các quy tắc của 2 hệ thống này sẽ cho ta một phương tiện hợp lý để chứng minh tính đúng đầy đủ của đoạn chương trình.
Hệ quả của định nghĩa.
+ Đặc tả { WP(S,Q) } S { Q } thỏa có điều kiện (đcđk)
+ WP(S,Q) bảo đảm tính dừng của S .Tức là S hoạt động đúng thực sự với đkđ WP(S,Q) và đkc Q .
+ WP(S ,Q ) là tân từ yếu nhất thỏa đầy đủ đặc tả {P} S {Q} . Tức là nếu có
tân từ P* bảo đảm S dừng và đặc tả {P*} S {Q} đúng có điều kiện thì P* ==>
WP(S,Q) hay { P *} ⊆ { WP(S,Q) } ( {WP(S,Q) } là tập điều kiện đầu lớn nhất
mà xuất phát từ đó thi hành S thì sẻ dừng tại trạng thái thỏa Q ) .
Đây là các dấu hiệu đặc trưng để nhận ra WP(S,Q)
Các ví dụ.
Tính WP(while n<>0 do n := n - 1, n = 0 ) và so sánh với tân từ yếu nhất thỏa có điều kiện lệnh lặp while n<>0 do n := n - 1 với điều kiện cuối n = 0 + Dựa vào quy luật của Hoare thì ta có :
{true} while n<>0 do n := n -1 { n = 0} Thực vậy :
Từ : {true and ( n<>0) } n := n-1 {true}
( xem bất biến vòng lặp là : I ≡ true )
ta suy ra : {true} while (n<>0) do n := n -1 {true and n = 0}
+ Từ đinh nghĩa WP ta suy ra :
wp (while (n<>0) do n := n -1 , n = 0 ) ≡ ( n >= 0 )
Ta có :
wp (while (n<>0) do n := n -1 , n = 0) ===> true
Tức là : tân từ yếu nhất thỏa đầy đủ đặc tả {P} S {Q} mạnh hơn tân từ yếu nhất
thỏa có điều kiện đặc tả ( tức là tập điều kiện đầu lớn nhất thỏa đầy đủ là tập con của tập điều kiện đầu thỏa có điều kiện )
S ≡ i := 0 ; Q ≡ ( i = 0 ) ;
Tìm wp (S,Q) .
Vì : + P ==> true với mọi P nên ta cũng có wp(S,Q) ==>true (a)
+ true bảo đảm S dừng và mọi trạng thái đầu đều dẫn đến Q nên true ==> wp(S,Q) (b)
Từ (a),(b) ta suy ra : wp(i:=0, i = 0) ≡ true Ví dụ 3 :
S ≡ i := 0 ; Q ≡ ( i = 1 ) ;
Tính wp (S,Q) .
Đây là trường hợp ngược với ví dụ 2. Bất chấp trạng thái trước lệnh gán là gì,
lệnh gán i := 0 không thể nào bảo đảm i=1.
Vì vậy : wp(i:= 0 , i=1) ≡ false
false mô tả tập hợp trạng thái rỗng. Tức là tập điều kiện đầu thỏa S,Q là tập rỗng .
Quan hệ giữa WP đối với các toán tử logic cấu tạo nên tân từ Q như thế nào?
Các quy ước :
Luật loại trừ trường hợp kỳ dị (The law of the excluded miracle ).
WP(S,false) ≡ false
WP(S,true) là tân từ xác định tập các trạng thái bảo đảm tính dừng của S
WP(while (n<>0 ) do n := n -1, true) ≡ ( n >= 0 )
Tính phân phối của and :
wp(S,Q) and wp(S,R) ≡ wp(S,Q and R)
Tính phân phối của or :
wp(S,Q or R) ≡ wp(S,Q) and wp(S,R)
Nếu Q ==> R thì wp(S,R) ==> wp(S,R)
Toán tử gán (tiên đề gán).
WP(x := bt , Q(x)) = Q(bt )
WP(i := i -1, i = 0) ≡ ( i-1 = 0 ) ≡ ( i = 1 ) .
WP(i := (l+u) div 2, l <= i <= u) ≡ l <= ((l+u) div 2) <= u
WP(i := 1, i =1 ) ≡ 1 = 1 ≡ true
Toán tử tuần tự.
WP( S1 ; S2 , Q) ≡ WP(S1 , WP(S2,Q))
WP(x := x+1 ; y := y+1 , x = y) ≡ WP(x := x+1 ; WP(y := y+1,x = y))
≡ WP(x:=x+1, x=y+1)
≡ x+1 = y+1 ≡ ( x = y)
Quy luật này hàm ý rằng tổ hợp tuần tự các lệnh có tính kết hợp (associativity)
tức là (S1 ; S2); S3 thì cũng cùng ý nghĩa với S1; (S2;S3).
Bởi vì với Q tuỳ ý wp((S1;S2);S3,Q) ≡ wp(S1 ; S2 , wp(S3,Q))
≡ wp(S1 , wp(S2, wp(S3,Q))) ≡ wp(S1 , wp(S2;S3,Q))
≡ wp((S1 ; (S2;S3)) ,Q)
Chứng minh tính đúng đầy đủ đặc tả sau : { S=i*(i+1)/2 }
i := i+1;
S := S+i;
{ S = i*(i+1)/2 }
Ta có :
wp(i := i+1 ; S := S+i, S=i*(i+1)/2)
≡ wp(i := i+1, wp(S := S+i, S=i*(i+1)/2))
≡ wp(i := i+1, S+i = i*(i+1)/2)
≡ S +i+1 = (i+1)*(i+1)+1)/2
≡ S = i*(i+1)/2)
Theo định nghĩa của wp ta có :
{ wp(i := i+1 ; S := S+i, S=i*(i+1)/2) }
i := i+1;
S := S+i;
{ S = i*(i+1)/2 }
đúng đầy đủ . Suy ra ĐPCM.
Toán tử điều kiện.
a)
WP(if B then S1 else S2, Q) ≡ (B ==> WP(S1 , Q) and (not B ==> WP(S2 , Q) )
Tính WP(if ( i= 0) then j := 0 else j := 1, j=1)
Ta có : WP(j := 0, j = 1) ≡ (1 = 0 ) ≡ false
WP(j := 1 , j = 1) ≡ (1 = 1 ) ≡ true
Nên : WP(if ( i = 0) then j := 0 else j := 1, j=1)
≡ ((i = 0) ==> false) and ((i<>0) ==> true)
≡ ( not(i=0) or false) and true ≡ ( i <> 0 )
Tính WP(if ( i>j ) then j := j+1 else i := i+1, i >= j)
Ta có : WP(j := j+1, i >= j) ≡ i >= j+1 ≡ i > j
WP(i := i+1 , i >= j) ≡ i+1 >= j ≡ i >= j -1
Nên WP(if ( i>j ) then j := j+1 else i := i+1, i >= j)
≡ ((i > j) ==> (i > j)) and ((i <= j) ==> (i >= j -1))
≡ true and ( not(i <= j) or (i >= j -1))
≡ (i > j) or ( i >= j - 1) ≡ ( i > j )
Định lý sau đây chứng minh sự đúng đắn của toán tử điều kiện nếu chấp nhận hệ tiên đề của Hoare và tính dừng.
Định lý :
Gọi P ≡ ( B==> WP(S1 ,Q )) and (not B ==> WP(S2 , Q) )
Thì ta có : + {P} if B then S1 else S2 {Q} đ cđk (1)
và + Với giả định S1 và S2 dừng nếu {R} if B then S1 else S2 {Q}
thì R ==> P ( P là tân từ yếu nhất thỏa đầy đủ đặc tả ) (2)
( Tức là : WP(if B then S1 else S2 , Q ) ≡ P
≡ ( B==> WP(S1 ,Q )) and (not B ==> WP(S2
Q) ) Chứng minh :
Theo định nghĩa của WP, nếu R ==> WP(S,Q) thì {R} S {Q} thỏa cđk
Mà ta có P and B ≡ B and WP(S1 ,Q )) ==> WP(S1 ,Q )
Vì vậy : {P and B} S1 {Q} thỏa cđk
Tương tự {P and (notB)} S2 {Q} thỏa cđk
Do đó, theo luật về lệnh chọn của Hoare, ta có : {P} if B then S1 else S2 {Q}
(1)
Giả sử S1 và S2 luôn luôn dừng và {R} if B then S1 else S2 {Q}
Thì : {R and B} S1 {Q}
{R and (not B)} S2 {Q}
và : if B then S1 else S2 luôn luôn dừng.
Vì vậy theo định nghĩa của WP ta có : R and B ==> WP(S1 ,Q )
và R and (notB) ==> WP(S2 ,Q )
Hai khẳng định trên tương đương với : R ==> (B ==> WP(S1 ,Q ) )
và R ==> (not B ==> WP(S2 ,Q ) )
Vì vậy R ==> (B ==> WP(S1 ,Q ) ) and (not B ==> WP(S2 ,Q )) ) (2)
Từ (1) và (2) ta suy ra : P ≡ WP(if B then S1 else S2 , Q ) .
Ta cũng có khẳng định ngược lại : Nếu chấp nhận tiên đề :
WP(if B then S1 else S2, Q) ≡ (B ==> WP(S1, Q) and (not B ==> WP(S2,Q))
thì có thể chứng minh luật về lệnh chọn của Hoare là đúng : Định lý : Giả sử S1, S2 dừng.
Nếu {P and B} S1 {Q}
và {P and not B1} S2 {Q}
thì {P} if B then S1 else S2 {Q} đúng
Chứng minh : (Bài tập)
Toán tử lặp.
Xây dựng WP(while B do S ,Q ) .
Xét vòng lặp W ≡ while B do S , với đkc Q.
Xây dựng tân từ : WP(while B do S, Q)
Nó phải bảo đảm W dừng sau một số hữu hạn lần lặp lại S và tới trạng thái thỏa Q .
Gọi k là số lần lặp (số lần thực hiện lệnh S ở thân vòng lặp). Ta xây dựng quy nạp
theo k :
Bước 0 : ( k = 0 ) tân từ yếu nhất mô tả tập lớn nhất các trạng thái bảo đảm S lặp
đúng 0 lần và tới trạng thái thỏa Q là : Po ≡ (not B) and Q
Bước 1 : ( k = 1) tân từ yếu nhất mô tả tập lớn nhất các trạng thái bảo đảm S lặp đúng một lần và tới trạng thái thỏa Q là : P1 ≡ B and WP(S,Po )
( tức là sau khi thực hiện một lần S thì trạng thái chương trình sẽ thoả Po ).
Bước 2 : ( k = 2 ) tân từ yếu nhất mô tả tập lớn nhất các trạng thái bảo đảm S lặp
đúng 2 lần và tới trạng thái thỏa Q là : P2 ≡ B and WP(S,P1 )
( tức là sau khi thực hiện một lần S thì trạng thái chương trình sẽ thoả P1 ).
Bườc k : Một cách tổng quát với k >= 1 thì tân từ yếu nhất mô tả tập lớn nhất các
trạng thái bảo đảm S lặp đúng k lần và tới trạng thái thỏa Q là : Pk ≡ B and
WP(S,P k-1 )
Như vậy một trạng thái đầu làm W dừng ở một trạng thái thoả Q khi và chỉ khi nó
thoả khẳng định sau : ∃(k : k >= 0 : Pk )
Tức là : WP(while B do S , Q) ≡ ∃ (k : k >= 0 : Pk )
Mối liên hệ giữa toán tử lặp và tiên đề lệnh lặp của hệ luật Hoare Ta tách việc khảo sát tính đúng một vòng lặp thành hai phần :
+ Phần quan sát sự biến đổi của vòng lặp để dẫn tới khẳng định nó dừng (tính dừng ). + Phần quan sát sự bất biến của vòng lặp để chứng minh kết quả cuối cùng của nó (đcđk)
Với ý tưởng đó ta tách WP(W,Q) ( với W là while do S) thành các thành phần tương ứng và khảo sát mối quan hệ giữa WP(W,Q) và các khẳng định của hệ luật Hoare. ) Với lệnh bất kỳ S, điều kiện yếu nhất để đảm bảo S dừng là không ràng buộc gì sau khi dừng. Tức là WP(S,true) là tân từ mô tả tập hợp tất cả các trạng thái mà xuất phát từ đó thì bảo đảm S dừng.
Ta có : WP(W,true) ≡ ∃ (k : k >= 0 :P k )
Với Po ≡ (not B) and true ≡ (not B)
Pk ≡ B and WP(S,Pk-1 ) với k > 0
( Po là điều kiện để không thực hiện S lần nào, P1 là điều kiện để thực hiện S
đúng một lần , Pk là điều kiện để thực hiện S đúng k lần.
W ≡ while ( n <> m) do begin
j := j* i ; k := k+j ; n := n+1 ;
end ;
Ta tính điều kiện đầu để W dừng như sau :
Po ≡ not (n <> m) ≡ ( n = m )
P1 ≡ B and WP(S,Po) ≡ ( n <> m) and ( n+1 = m ) ≡ ( n+1 = m )
Giả thiết quy nạp rằng Pk ≡ (n+k = m) .
Ta có :
Gỉa thiết đúng với k = 0 vì Po ≡ (n = m) ≡ ( n + 0 = m )
Gỉa sử gỉa thiết đã đúng với k . Tức là : Pk ≡ ( ( n+k ) = m )
Chứng minh gỉa thiết đúng với k+1. Thực vậy:
Pk+1 ≡ B and WP(S,Pk ) ≡ ( n <> m) and ((n+1)+k = m) ≡ ( n+(k+1) = m)
( WP(S,Pk ) ≡ WP (j := j* i ; k := k+j ; n := n+1 ,( (n + k ) = m ) ) = (n + ( k +1))
= m )
Vậy : Pi ≡ ( n+i = m )
Tức là : WP(W,true) ≡ ∃ (i: i>=0; n+i =m) ≡ ( n >= m )
) Quan hệ giữa { P } S { Q } và WP(S,Q)
Theo định nghĩa về tính đúng và WP (S , Q ) ta có : S đúng có điều kiện dựa trên điều kiện đầu P và điều kiện cuối Q ( đặc tả {P} S {Q} đcđk) nếu và chỉ nếu hội
(and ) của P và điều kiện yếu nhất bảo đảm sự dừng của S mạnh hơn điều kiện yếu nhất bảo đảm S dừng trong một trạng thái thoả tân từ Q.
Tức là : {P} S {Q} thỏa cđk khi và chỉ khi P and WP(S,true) ==> WP(S,Q)
Như vậy :
{ I and B } S { I } thỏa có đk khi và chỉ khi I and B and WP(S,true) ==> WP(S,I)
{I} while B do S {I and not B} thỏa có đk khi và chỉ khi
{I} and WP(while B do S , true) ==> WP(W, I and not B)
Như vậy chứng minh S giữ bất biến I chính là chứng minh I and B and wp(W,true) ==> wp(S, I)
Chứng minh W dừng ứng với đkđ P chính là chứng minh : P ==> WP(W,true)
Định lý bất biến cơ sở (Fundamental invariance theorem) của Dijkstra phát biểu một dạng khác của luật về vòng lặp của Hoare .
Định lý: Giả sử I and B and WP(S,true) ==> WP(S,I) ( I là bất bất biến của vòng
lặp )
thì : I and WP(W,true) ==> WP(while B do S , I and notB )
({I} while B do S {I and not B} )
Chứng minh : Ta sẽ chứng minh bằng quy nạp trên k rằng
I and Pk (true) ==> Pk(I and not B ) (a)
với : Po(Q) ≡ not B and Q
Pk(Q) ≡ B and wp(S, Pk-1(Q))
Chú ý là Pk(Q) là đkđ yếu nhất bảo đảm vòng lặp while B do S dừng sau đúng k lần lặp trong một trạng thái thoả mãn Q.
(i) Cơ sở I and Po(true) ≡ I and (not B and true ) (định nghĩa)
≡ not B and ( I and not B) ≡ Po(I and not B)
(ii) Bước quy nạp : Giả sử (a) đã đúng với k . Tức là :
I and Pk(true) ==> Pk(I and not B)
Ta chứng minh (a) đúng với k+1 .
Thực vậy : I and Pk+1(true)
WP(S,Pk(true))
WP(S,Pk(true)) )
WP(S,Pk(true))
≡ I and B and WP(S,Pk(true)) (định nghĩa)
≡ B and I and B and WP(S,Pk(true)) ≡ B and I and B and WP(S,true) and
( vì WP(S,Pk(true)) ≡ WP(S,true) and
≡ B and ( I and B and WP(S,true) ) and
==> B and WP(S,I) and WP(S,Pk(true))
( I and B and WP(S,true) ==> WP(S , I ) gỉa thiết I là bất biến )
≡ B and WP(S,I and Pk(true)) (phép phân phối _and)
==> B and WP(S,Pk(I and not B))
( vì : I and Pk(true) ==> Pk(I and not B giả thiết quy nạp và tính chất phép phân phối
==>)
≡ Pk+1(I and not B)
Tức là: I and Pk(true) ==> Pk+1(I and not B)
Theo nguyên lý quy nạp ta suy ra :
I and Pk(true) ==> Pk(I and not B) với mọi k >= 0
Từ điều này ta có :
I and WP(W, true) ≡ I and (k : k >= 0 : Pk(true))
≡ (k : k >= 0 : I and Pk(true))
==> (k : k >= 0 : Pk(I and not B)) ≡ WP(W,I and not B)
Ta có đpcm.
Lược đồ kiểm chứng.
Để chứng minh tính đúng của đặc tả đoạn chương trình người ta thường :
- Thiết lập các khẳng định về trạng thái chương trình ở các điểm trung gian cần thiết.
- Chứng minh tính đúng của các khẳng định đó.
Những khẳng định về trạng thái chương trình ở những điểm trung gian không chỉ nhằm phục vụ việc kiểm chứng mà còn có mục tiêu là giúp người sử dụng chương trình hiểu được ngữ nghĩa của đoạn chương trình . Tức là góp phần xây dựng một chương trình có dạng thức tốt ( dễ đọc, dễ hiểu ). Nghệ thuật của việc chứng minh tính đúng của chương trình và xây dưng sưu liệu cho chương trình ( ở đây là đưa ra những ghi
chú vào chương trình) là ở chỗ làm sao chèn vào các khẳng định trung gian vừa đủ : quá nhiều sẽ làm khó đọc, mất nhiều thời gian kiểm tra, còn quá ít thì không đủ đặc tả ngữ nghĩa .
Trong phần này ta thảo luận ý tưởng chứng minh tính đúng của đoạn chương trình trong dạng lược đồ kiểm chứng tính đúng (Proof tableaux).
Các khái niệm.
- Lược đồ kiểm chứng tính đúng (lđkc) của một đoạn chương trình là một dãy đan xen giữa các khẳng định (assertion) và lệnh (statement) của đoạn chương trình,
với bắt đầu và kết thúc bởi các khẳng định.
- Một lược đồ kiểm chứng là đúng (valid) nếu khi ta bỏ đi các khẳng định trung
gian thì nó trở thành một đặc tả đúng. Từ những kiến thức đã trình bày ở các phần trên
ta suy ra: Một lược đồ kiểm chưng là đúng khi và chỉ khi :
+ Mọi bộ đặc tả dạng {P} S {Q} xuất hiện trong lđkc đều là những
đặc tả đúng.
+ Mọi cặp khẳng định đứng liền nhau dạng {H} {T} trong lđkc thì
đều thỏa quan hệ P ==> Q đúng.
Từ định nghĩa trên ta thấy : một lđkc có thể biến dạng theo nhiều mức chi tiết. Từ một bộ ba đặc tả gồm : đoạn lệnh S , tân từ mô tả điều kiện đầu P , tân từ mô tả điều
kiện cuối Q ( đặc tả {P} S {Q} ) ta có thể xây dựng nhiều dạng lđkc khác nhau bằng
các cách chèn khác nhau các khẳng định trung gian .
Dạng thô nhất của lđkc chính là đặc tả tính đúng của đoạn chương trình nó chỉ chứa 2 khẳng định : một ở đầu đoạn chương trình và một ở cuối đoạn chương trình . Dạng min nhất của lđkc là lđkc mà mọi lệnh đều bị kèm giữa hai khẳng định ( đặc tả ngữ nghĩa tới từng câu lệnh ) nó là lược đồ kiểm chứng ở mức chi tiết nhất (lược đồ kiểm chứng chi tiết - lđkcct).
Trung gian giữa hai dạng lđkc trên người ta thường sử dụng lđkc chỉ có các khẳng định trung gian ở những chỗ cần thiết ( những chổ quan trọng , những chổ ngoặt trong nội dung ngữ nghĩa của đoạn chương trình ).
Kiểm chứng tính đúng.
Ý tưởng
Để kiểm chứng tính đúng đặc tả của đoạn chương trình S . Tức là khẳng định đặc tả {P} S {Q} đúng . Ta cần thực hiện các việc sau:
+ Xây dựng lđkc hợp lý xuất phát từ đặc tả của đoạn chưong trình . + Chứng minh tính đúng của lđkc vừa xây dựng .
Trong 2 công việc trên thì việc xây dựng lđkc hợp lý là việc tốn nhiều thời gian và công sức . Việc xây dựng lược đồ chưng minh hợp lý sẻ khác nhau phụ thuộc vào cấu trúc của đoạn lệnh S song thường được tiến hành theo 2 bước sau :
Bước 1 : Từ đặc tả xây dựng lược đồ trung gian (chi tiết hay gần chi tiết ) dựa vào các tiên đề (của hệ Hoare hoặc của hệ Dijkstra ) mô tả ngữ nghĩa của từng lệnh bằng cách chèn vào các khẳng định trung gian .
Bước 2 : Từ dựng lược đồ trung gian (chi tiết hay gần chi tiết ) dựa vào các tiên đề (của hệ Hoare hoặc của hệ Dijkstra ) mô tả ngữ nghĩa của từng lệnh bỏ bớt các khẳng đinh trung gian tầm thường ( các khẳng định ở những vị trí không quan trong , các khẳng định mà tính đúng của chúng là rõ ràng và dang thức của chúng đơn giản dễ dàng khôi phục lại khi cần ) . Giữ lại khẳng định trung gian nào trong lđkc hợp lý là một trong những nghệ thuật của người kiểm chứng nó phản ánh rõ nét mức trí tuệ (khả năng tư duy, kiến thức tích lũy ) của người kiểm chứng .
Việc chứng minh tính đúng đầy đủ của lđkc phụ thuộc vào cấu trúc đoạn lệnh S và hệ tiên đề mà ta đã sử dụng để xây dựng lược đồ kiểm chứng hợp lý. - Trương hợp 1 : Nếu đoạn lệnh S không chứa một lệnh lặp nào cả thì tính dừng được xem là hiển nhiên, khi đó 2 hệ tiên đề là hoàn toàn tương đương . - Trường hợp 2 : Nếu đoạn lệnh S có chứa lệnh lặp thì tính dừng không phải bao giờ cũng được thỏa nên ta cần phải chỉ ra . Khi đó 2 hệ tiên đề là không tương đương .
+ Nếu trong suốt qúa trình xây dựng lược đồ kiểm chứng ta chỉ sử dụng hệ tiên đề Dijikstra thì không phải kiểm chứng lại tính dừng nữa .
+ Nếu trong qúa trình xây dựng lược đồ kiểm chứng ta có sử dụng (dù chỉ một lần ) tiên đề của hệ Hoare thì phải kiểm chứng lại tính dừng ( vì tiên đề Hoare không bảo đảm tính dừng ) .
Kiểm chứng tính đúng đặc tả {P} S {Q} khi S là một dãy lệnh tuần tự.
( S ≡ { S1 ; S2 ; .. . ; Sn } )
Kiểm chứng tính đúng đặc tả : { P } S1 ; S2 ; .. . ; Sn { Q }
Kiểm chứng đặc tả :
{even(k) and (0 < k ) and (y*zk = xn )} (1) k := k div 2 ;
z := z*z ;
{(0 <= k ) and (y * zk ) = xn )} (2)
Bài giải :
Cách 1 : Xây dựng lđkc hợp lý dựa vào hệ Haore . -Bước 1 : Xây dựng lược đồ kiểm chứng hợp lý. + Xây dựng lược đồ kiểm chứng chi tiết : Từ (1) ta suy ra :
{even(k) and ( 0 < k ) and (y * zk ) = xn )} (2a)
{(0 <= k div 2 ) and (y * (z*z)k div 2 = xn ) } (2d)
k := k div 2 ; (2)
{(0 <= k ) and (y * (z*z)k = xn ) } (2c)
z := z*z ;
{(0 <= k ) and (y * zk = xn ) } (2b)
Diễn giải : Từ (2b) và lệnh gán z := z*z dùng tiên đề gán ta suy ra (2c)
Từ (2c) và lệnh gán k := k div 2 dùng tiên đề gán ta suy ra (2d)
+ Xây dựng lđkc hợp lý từ lđkc chi tiết :
Từ (2) ta suy ra :
{even(k) and ( 0 < k ) and (y * zk ) = xn )} (2a)
{(0 <= k div 2 ) and (y * (z*z)k div 2 = xn ) } (2d)
k := k div 2 ; (3)
z := z*z ;
{(0 <= k ) and (y * zk = xn ) } (2b)
Diễn giải : Từ (2b),(2c),(2d) và 2 lệnh gán tuần tự z := z*z ; k := k div 2 dùng
tiên đề tuần tự ta bỏ đi (2c)
- Bước 2 : chứng minh lđkc hợp lý (3) đúng :
{(0 <= k div 2 ) and (y * (z*z)k div 2 = xn ) } (2d)
k := k div 2 ; (3a)
z := z*z ;
{(0 <= k ) and (y * zk = xn ) } (2b)
Ta có : Tính đúng của (3a) được khẳng định dựa vào cách xây dựng . Kiểm chứng hai khẳng định đi liền nhau :
{ even(k) and ( 0 < k ) and (y * zk ) = xn ) } {( 0 <= k div 2 ) and (y*(z*z)kdiv 2 = xn ) }
có quan hệ hàm ý (==>) (hiển nhiên) (3b).
Từ (3a),(3b) áp dụng luật hệ quả ta suy ra (3) đúng .
Nhân xét :
Ta có thể hình thức hóa quá trình chứng minh bằng cách đưa vào ký hiệu :
I(z,k) ≡ ( 0 <= k ) and (y*z k= xn )
Khi đó (2) có thể viết thành :
{even(k) and (0<k) and I(z,k)} {I(z*z,k div 2 )}
k:=k div 2 ; {I(z*z,k )}
z := z*z ; {I(z,k)}
(3) có thể viết thành :
{even(k) and (0<k) and I(z,k)} {I(z*z,k div 2 )}
k := k div 2 ; z := z*z ;
{I(z,k)}
Điều kiện cần kiểm chứng là :
even(k) and (0<k) and I(z,k) ⇒ I(z*z,k div 2 )
Chú ý : Khi có một cặp {P} {Q} xuất hiện trong lược đồ thì khẳng định hàm ý
(===> ) tương ứng là một điều kiện cần kiểm chứng (đkckc - verification
condition). Các điều kiện này là cốt lõi của chứng minh về tđcđk, phần còn lại của
chứng minh chỉ là việc áp dụng máy móc các quy luật.
Trong ví dụ trên, đkckc là :
even(k) and (0 < k ) and I(z,k)} ==> I(z*z , k div 2)
Đây chỉ là cách nói hình thức của sự kiện là (z*z)k div 2
chẵn.
Cách 2 : Xây dựng lđkc hợp lý dựa vào hệ Dijkstra.
Bước 1 : Xây dựng lđkc hợp lý.
- Tính WP( k := k div 2 ; z := z*z , I(z,k))
Ta có : WP( k := k div 2 ; z := z*z , I(z,k))
≡ WP( k := k div 2 ,WP( z := z*z , I(z,k))
= zk khi k là số nguyên
≡ WP( k := k div 2 , I(z*z,k)) ≡ I(z * z , k div 2))
+ Chèn WP( k := k div 2 ; z := z*z , I(z,k)) vào (1) ta được lđcm hợp lý : {even(k) and (0<k) and I(z,k)}
{I(z*z,k div 2 )}
k := k div 2 ; z := z*z ;
{I(z,k)}
Bước 2 : Kiểm chứng tính đúng của lđkc hợp lý .
Ta có : {I(z*z,k div 2 )}
k := k div 2 ; z := z*z ;
{I(z,k)} (a) đúng
even(k) and (0<k) and I(z,k) ⇒ I(z*z,k div 2 ) (b) đúng.
Từ (a) , (b) ta suy ra đặc tả đúng
Kiểm chứng khi đoạn chương trình có chứa câu lệnh điều kiện
{P} if B then S1 else S2 {Q}
Khi đó ta thêm các khẳng định trung gian dạng:
{P} if B then {P and B} S1 {Q}
else {P and not B} S2 {Q}
( hoặc :
{P} if B then {P and B} S {Q}
else {P and not B} {Q}
khi không có phần else )
vào nơi có lệnh điều kiện tương ứng ta có lđkc trung gian thích hợp . Ví dụ : Kiểm chứng đoạn chương trình :
{(0 < k ) and ( y * zk = xn}
if even(k) then begin
k := k div 2 ;
z := z*z ;
end
else begin
k := k -1 ;
y := y*z ;
end
{(0 <= k ) and ( y * zk = xn )}
Cách 1: Dùng hệ tiên đề Hoare.
+ Bước 1 : Xây dựng lđkc hợp lý.
Đặt I(y,z,k) ≡ ( 0 <= k) and (y*z k= xn )
Đặc tả có dạng : {(0 < k ) and I(y,z,k)}
if even(k) then begin
k := k div 2 ;
z := z*z ;
end
else begin
k := k -1 ;
y := y*z ;
end
{I(y,z,k)}
Chèn các khẳng định trung gian (dựa vào tiên đề gán của Hoare)
{(0 < k ) and I(y,z,k)}
if even(k) then {even(k) and (0 < k ) and I(y,z,k)}
begin
{ I(y ,z*z , k div 2 ) } k := k div 2 ;
{ I( y , z*z , k ) } z := z*z ;
end;
{I(y,z,k)}
else
{(not even(k)) and (0 < k ) and I(y,z,k)} begin
{ I(y*z ,z , k -1) } k := k -1 ;
{ I(y*z , z , k ) } y := y*z ;
end
{I(y,z,k)}
Bỏ đi các khẳng định trung gian tầm thường (dựa vào luật tuần tự của Haore) ta có
lđkc hợp lý : {(0 < k ) and I(y,z,k)}
if even(k) then {even(k) and (0 < k ) and I(y,z,k)}
{ I(y ,z*z , k div 2 ) }
begin k := k div 2 ; z := z*z ;
end
{I(y,z,k)}
else
{(not even(k)) and (0 < k ) and I(y,z,k)} { I(y*z ,z , k -1) }
k := k -1 ;
y := y*z ; {I(y,z,k)}
+ Bước 2: Chứng minh lược đồ kc đúng.
Các cặp khẳng định đứng liền nhau xuất hiện trong lược đồ :
{even(k) and (0 < k ) and I(y,z,k)} { I(y ,z*z , k div 2 ) } (a) và {(not even(k)) and (0 < k ) and I(y,z,k)} { I(y*z ,z , k -1) }(b) Các hàm ý tương ứng cần phải chứng minh đúng :
{even(k) and (0 < k ) and I(y,z,k)} ==> { I(y ,z*z , k div 2 ) } (a*)( kiểm chứng ? )
và {(not even(k)) and (0 < k ) and I(y,z,k)} ==> { I(y*z ,z , k -1) }(b*) ( Kiểm chứng ? )
Từ (a*) và (b*) ta suy ra điều phải kiểm chứng.
Cách 2: Dùng hệ tiên đề Dijkstra.
- Bước 1 : Xây dựng lđkc hợp lý.
Đặt I(y,z,k) ≡ ( 0 <= k) and (y*z k= xn )
S1 ≡ begin k := k div 2 ; z := z*z ; end ;
S2 ≡ begin k := k -1 ; y := y*z ; end ;
B ≡ even(k)
Đặc tả có dạng : {(0 < k ) and I(y,z,k)}
if B then S1 else S2
{I(y,z,k)}
+ Tính WP(if B then S1 else S2 , I(y,z,k) )
≡ ( B ==> WP(S 1, I(y,z,k) ) ) and (not B ==> WP(S2 , I(y,z,k) ) )
≡ ( dành cho người đọc )
+ Chèn khẳng định WP(if B then S1 else S2 , I(y,z,k) ) vào đặc tả theo tiên đề chọn cùa Dijkstra ta được lđkc hợp lý dạng :
{(0 < k ) and I(y,z,k)}
{ WP(if B then S1 else S2 , I(y,z,k) ) }
if B then S1 else S2
{I(y,z,k)}
- Bước 2 : Chứng minh lđkc đúng.
Cặp khẳng định đứng liền nhau trong lđkc là :
{(0 < k ) and I(y,z,k)} { WP(if B then S1 else S2 , I(y,z,k) ) }
Ta cần chứng minh tính đúng của hàm ý tương ứng :
{(0 < k ) and I(y,z,k)} ==> { WP(if B then S1 else S2 , I(y,z,k) ) } (*)
( CM * danh cho người đọc )
Từ (*) suy ra điều phải kiểm chứng.
Kiểm chứng khi đoạn chương trình có chứa lệnh lặp while B do S.
Cách thứ 1: Sử dụng hệ tiên đề Dijkstra.
- Bươc 1 : Xây dựng WP(While B do S ) và chèn vào trước lệnh lặp .
{ WP(while B do S } while B do S
- Bườc 2: Xây dựng lđkc hợp lý từ lđkc trên.
- Bước 3 : Chứng minh tính đúng của các điều kiện cần kiểm chứng.
Cách thứ 2 : Sử dụng hệ tiên đề Hoare.
- Bươc 1 : Phát hiện bất biến I của vòng lặp và chèn các khẳng định trung
gian tương ứng vào trước giữa và sau lệnh lặp ( tiên đề Haore) .
{(Invariant) I}
while B do
{I and B} S {I}
{I and not B }
- Bườc 2. Xây dựng lđkc hợp lý từ lđkc trên.
- Bước 3 : Chứng minh tính đúng của các điều kiện cần kiểm chứng .
Bước 4 : Chứng minh lệnh lặp dừng . Ví dụ : Kiểm chứng đặc tả : { 0 <= n }
y := 1 ; z := x ; k := n ; while (0 <> k ) do begin
k := k -1 ; y := y*z end
{y = xn }
Biết bất biến của vòng lặp : I(y,z,k) ≡ ( k >= 0 ) and ( y*z = xn )
Bài giải theo cách 1:
Dựa vào hệ Hoare ta xây dựng lđkc chi tiết xuất phát từ điều kiện đầu , điều kiện cuối và bất biến
{0 <= n}
{I(1,x,n)} y := 1 ;
{I(y,x,n)} z := x ;
{I(y,z,n)}
k := n ;
{ I(y,z,k)}
while (0 <> k ) do begin
{I(y,z,k) and (k <> 0 )} {I(y*z,z,k-1)}
k := k -1 ;
{I(y*z,z,k)} y := y*z ; {I(y,z,k)} end
{I(y,z,k) and (k = 0 )} {y = xn }
Bỏ đi các khăng định trung gian tầm thường ta có lđcm hợp lý dạng : {0 <= n}
{I(1,x,n)} y := 1 ;
z := x ; k := n ;
{ I(y,z,k)}
while (0 <> k ) do begin
{I(y,z,k) and (k <> 0 )} {I(y*z,z,k-1)}
k := k -1 ;
y := y*z ; {I(y,z,k)} end
{I(y,z,k) and (k = 0 )} {y = xn }
Các điều kiện cần kiểm chứng là : (0 <= n ) ==> I(1,x,n)
I(y,z,k) and (k = 0 ) ==> y = xn .
I(y,z,k) and (k <> 0 ) ==> I(y*x,z,k-1)
Thay I(y,z,k) ≡ (0 <= k) and ( y * z k = xn ) ba đkckc trên sẽ trở thành :
(Phần chuẩn bị) ( 0 <= n ) ==> (1*xn = xn )and (0 <= n ) (hiển nhiên )
(Phần kết thúc lặp) ( y * zk = xn ) and (0 <= k ) and (k = 0 )==> y = xn (hiển nhiên)
(Phần thân vòng lặp) ( y * zk = xn ) and (0 <= k ) and (k <> 0 )
==> ((y*z)*zk-1 = xn ) and (0 <= k -1)
≡ ( y * zk = xn ) and (0 < k )
==> (y*zk = xn ) and (0 <= k -1) (hiển nhiên )
Một lđkc đầy đủ trong đó mỗi lệnh đều được kèm giữa hai khẳng định rõ ràng là chi tiết quá mức. Thực ra sử dụng tri thức của ta về các đkđ yếu nhất của những lệnh khác lệnh lặp, ta có thể mô tả một giải thuật để sản sinh ra một chứng minh hoàn chỉnh theo kiểu Hoare về tính đúng có điều kiện của đoạn lệnh S dựa trên điều kiện đầu P và điều kiện cuối Q, với giả định là mỗi vòng lặp while trong S được cung cấp kèm theo bất biến của nó.
Về nguyên tắc, một bộ chứng minh định lý tự động (theorem prover), với khả năng kiểm chứng các điều kiện có dạng P ==> R có thể được dùng để chứng minh một cách tự động tđcđk của 1 đoạn chương trình . Điểm quan trọng mà ta rút ra từ các phần đã trình bày là: phần cốt lõi trong một chứng minh về tđcđk là việc phát hiện ra các bất biến và sau đó việc kiểm chứng các điều kiện hàm ý nhằm sử dụng luật hệ quả.
Chúng ta không mô tả giải thuật để sản sinh các chứng minh kiểu Hoare, thay vào đó, ta sẽ trừu tượng hoá từ nó quá trình sản sinh ra tập hợp các điều kiện cần kiểm chứng.
Xét một đoạn CT bất kỳ với các đkđ P và đkc Q. Ta sẽ xây dựng từ P, S và Q bằng quy nạp một điều kiện đầu yếu nhất dựa vào S và Q, ký hiệu là pre(S,Q), và hai tập hợp các điều kiện cần kiểm chứng V'(S,Q) and V(P,S,Q) như sau :
1. Nếu S là lệnh gán x := bt thì pre(S,Q) là WP(S,Q) và V'(S,Q) rỗng.
Tức là : pre( x := bt ,Q(x) ) ) ≡ WP(x := bt ,Q(x)) ≡ Q(bt) và V'(x := bt ,Q) ≡ ∅.
2. Nếu S có dạng S1 ; S2 thì pre(S,Q) là pre(S1, pre(S2,Q)) và V'(S,Q) là hội
của
V'(S2 , Q) và V'(S1 ,pre(S2 ,Q)).
Tức là : pre(S1; S2 , Q) ≡ pre(S1, pre(S2,Q))
Và V'(S1; S2 ,Q) ≡ V'(S2 , Q) ∪ V'(S1 ,pre(S2 ,Q)).
3. Nếu S có dạng if B then S1 else S2 thì pre(S,Q) là :
(B and pre(S1,Q)) or (not B and pre(S2,Q)) và V'(S,Q) là hội của V'(S1,Q) và V'(S2,Q).
Tức là : pre(if B then S1 else S2 ,Q) ≡ (B and pre(S1 ,Q)) or (not B and pre(S2
,Q)) Va V'(if B then S1 else S2 ,Q) ≡ V'(S1,Q) ∪ V'(S2,Q).
4. Nếu S có dạng while B do S1 và I là bất biến của vòng lặp thì pre(S,Q) là I, và V'(S ,Q) là hội của V(I and B , S1 ,I) và tập hợp chỉ gồm một điều kiện I and not B ==> Q.
Tức là : pre(S,Q) ≡ I và V'(S ,Q) ≡ V(I and B , S1 ,I) ∪{ I and not B ==> Q }.
5. Trong mọi trường hợp V(P,S,Q) là hội của V'(S,Q) và tập hợp chỉ gồm một điều kiện P ==> pre(S,Q).
Tức là : V(P,S,Q) ≡ V'(S,Q) ∪ { P ==> pre(S,Q) }.
Các chức năng của pre(S,Q) , V'(S, Q) ,và V(S,P,Q) trong quá trình này được mô tả bởi các mệnh đề sau :
(P1) Nếu mọi đkckc trong tập hợp V(S,Q) đều đúng thì S là đcđk dựa trên đkđ pre(S,Q) và đkc Q. Tức là : { pre(S,Q) } S { Q } đúng có điều kiện.
(P2) Nếu mọi đkckc trong tập hợp V(P,S,Q) đều đúng thì S là đcđk dựa trên đkđ P và đkc Q. Tức là : { P } S {Q } đúng có điều kiện.
Tính chất (P1) có thể được chứng minh bằng quy nạp trên kích thước của S, ở đây kích thước của S có được bằng cách đếm là 1 cho mỗi lần xuất hiện các ký hiệu ':=', ';', 'if', 'while' trong S. Tính chất (P2) là một hệ quả trực tiếp của (P1).
Chú ý rằng pre(S,Q) khác với wp(S,Q) chỉ khi có lệnh while. Điều này xác nhận là trong trường hợp tổng quát, không có khả năng tạo lập một công thức đóng cho đkđ yếu nhất của lệnh while và nhấn mạnh tầm quan trọng của việc ghi nhận những tính chất bất biến trong các sưu liệu chương trình.
Với đặc tả gồm :
Dẫy lệnh tuần tự S : S ≡ tg := tg + a[k] ; k := k+1 ;
đkc Q ≡ I(k, tg) ≡ (tg = S(i : 0 <= i < k : a[i]))
đkđ P ≡ I(k,s) and (k <> n )
Ta áp dụng các bước 1 và 2 được : V'(S, I(k, tg)) là rỗng .
pre(S, I(k, g)) là I(k+1, tg+a[k]) tập các đkckc
V(P,S,Q) ≡V(I(k,tg) and k <> n, S, I(k, tg)) chứa một điều kiện là I(k,tg) and k <> n ==> I(k+1, tg+a[k])
Tức là : ( tg = S(i : 0<= i< k : a[i])) and (k <> n )
==> tg + a[k] = S( i: 0 <= i <= k+1 : a[i]) (1)
Xét đặc tả đoạn chương trình tính tổng các phần tử của một array
{0 <= n}
k := 0 ; tg := 0 ;
{(Invariant ) I(k,tg) } ≡ { tg = S(i: 0<= i <k : a[i])}
while (k <> n ) do
begin
tg := tg + a[k] ; k := k+1 ; end
{tg = S(i: 0 <= i < n : a[i])}
Tách đoạn chương trình thanh 2 nhóm :
+ Nhóm lệnh tuần tự : So ≡ k := 0 ; tg := 0 ;
+ Lệnh while : W ≡ while k <> n do begin
tg := tg + a[k] ; k := k+ 1 end
Theo quy tắc 2, ta cần tính pre(W,Q) và V'(W,Q) với Q ≡ tg = S(i: 0 <= i < n : a[i])
Bây giờ, dùng quy tắc 4,
pre(W,Q) ≡ I(k,tg) ≡ tg = S(i : 0 <= i < k : a[i])
Cũng vậy V'(W,Q) bao gồm V(I(k,tg) and k <> n, S1, I(k,tg)) với S1 là nhóm lệnh trong vòng lặp, và điều kiện
I(k,tg) and (k = n )==> tg = S(i : 0<= i <n : a[i]) (2) Cuối cùng, ta có thể tìm được
pre(So, I(k,tg)) ≡ 0 = S(i: 0 <= i <0 : a[i])
và tập hợp các đkckc cho So bao gồm chỉ một điều kiện
( 0 <= n) ==> pre(So, I(k,tg)) (3)
Như vậy, có 3 đkckc cho CT, đó là các điều kiện (1), (2), (3).
