Kỹ thuật lập trình nâng cao - 59 -
CHƯƠNG V
KIỂM CHỨNG TÍNH ĐÚNG CÓ ĐIỀU KIỆN

I. CÁC KHÁI NIỆM VỀ TÍNH ĐÚNG.

Xét bộ 3 gồm : đọan lệnh S, các tân từ trên các biến của chương trình (có thể bao
gồm các biến giả) P, Q ( Pø mô tả điều kiện đầu , Q mô tả điệu kiện cuối ).
Bộ 3 : { P } S { Q } tạo nên đặc tả đoạn lệnh S .
Đặc tả : { P } S { Q } được gọi là thỏa đầy đủ ( đúng đầy đủ – đ đ đ ) nếu xuất
phát từ bất kỳ 1 trạng thái thỏa P thực hiện đoạn lệnh S thì việc xử lý sẻ dừng ở trạng
thái thỏa Q .
Đặc tả : { P } S { Q } được gọi là thỏa có điều kiện ( đúng có điều kiện – đcđk )
nếu xuất phát từ bất kỳ 1 trạng thái thỏa P thực hiện đoạn lệnh S nếu việc xử lý dừng
thì trạng thái cuối thỏa Q ( tính dừng của S chưa được khẳng đònh ).
Khẳng đònh { P } S { Q } diễn đạt tính đúng có điều kiện (condition
correctness) (tđcđk) của S. Tính đúng của S dựa trên đkđ P và đkc Q với giả đònh
rằng tính dừng của S đã có.
Ví dụ : a) { (x = x
o
) and (y = y
o
) } Nếu (x = x
o
) và (y = y
o
) trước khi
t := x t := x được thi hành
{( t = x = x
o

) and (x = y = yo ) } Nếu (t = x
o
) và (x = y = y
o
) trước khi
y := t y := t được thi hành
{( y = x
o
) and (x = y
o
) } Thì sau đó ( y = x
o
) và ( x = y
o
)
Các phát biểu a, b, c là đúng theo cảm nhận của ta về lệnh gán.
d) { x > 0 } Nếu (x > x
o
) trước khi
x := x-1 x := x-1 được thực hiện
{ x > 0 } Thì sau đó ( x > 0 )
Phát biểu d là sai vì có một trạng thái ban đầu x = 1 thoả P ( x > 0 ) nhưng sau
khi thi hành lệnh x := x -1 (x giảm 1) thì x = 0 không thoả Q ( x > 0 ) .

II. HỆ LUẬT HOARE (HOARES INFERENCE RULES). Trần Hoàng Thọ Khoa Toán - Tin

Kỹ thuật lập trình nâng cao - 60 -

1b.

Q => R , { P } S { Q }
–––––––––––––––––– (1b)
{ P } S { R }

Ví dụ 3 : 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)

Trần Hoàng Thọ Khoa Toán - Tin

Kỹ thuật lập trình nâng cao - 61 -
Ví dụ 4 : 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.

2. Tiên đề gán (The Assignement Axiom)

{ P(bt) } x := bt { P(x) } (2) Từ (2 ) ta suy ra nếu trước lệnh gán x := bt ; trạng thái chương trình làm P(bt) sai

, luật này phát biểu ý sau :
Nếu: i) Thi hành S
1
với đkđ P đảm bảo đkc R ( đặc tả { P } S
1
{ R } đ cđ k )
ii) Thi hành S
2
với đkđ R đảm bảo đkc Q ( đặc tả { R } S
2
{ Q } đ cđ k)
Thì : thi hành S
S
≡
1
; S
2
với đkđ P đảm bảo đkc Q (đ ặc tả { P } S
1
; S
2
{ Q } đ
cđ k )
Ví dụ : Kiểm chứng tđcđk đặc tả :

Trần Hoàng Thọ Khoa Toán - Tin

Kỹ thuật lập trình nâng cao - 62 -
{true} x := 5 ; y := 2 { x = 5, y = 2 }
Ta có : { 5 = 5 } x := 5 { x= 5} (a) // tiên đề gán

Và
{ P and notB } + Nếu xuất phát từ trạng thái thỏa P and not B
S
2
thi hành S
2
thì sẻ tới trạng thái thỏa Q
{ Q }
Thì suy ra :
{ P } Nếu xuất phát từ trạng thái thỏa P
if B then S
1
else S
2
thi hành lệnh if B then S
1
else S
2

{ Q } thì sẽ tới trạng thái thỏa Q .

b2)

{ P and B} S { Q} , P and (not B ) => Q
–––––––––––––––––––––––––––––––––––– (3.2b)
{ P } if B then S { Q} Ví dụ1 : Kiểm chứng tđcđk đặc tả :
{ i> 0 } if ( i= 0 ) then j := 0 else j := 1 {j=1}

true and not odd(x) ==> even(x) (d) // hiển nhiên
Từ (c) và (d) dựa vào 3.2b suy ra ĐPCM .

b3) Luật về lệnh lặp While { I and B } S { I }
––––––––––––––––––––––––– ------ (3.3)
{ I } while B do S { I and (not B ) } Luật này nói rằng nếu I không bò thay đổi bởi một lần thực hiện lệnh S thì nó
cũng không bò thay đổi bởi toàn bộ lệnh lặp While B do S. Với ý nghóa này I được gọi
là bất biến (invariant) của vòng lặp.
Chú ý rằng khẳng đònh : { P } while B do S { Q } thỏa dựa vào hệ luật Hoare
chỉ xác đònh tđcđk (conditionnal correctness). Để chứng minh tính đúng (correctness)
thực sự ta cần bổ sung chứng minh lệnh lặp dừng.
Ví dụ1 :
Kiểm chứng tính đúng có điều kiện của đặc tả :
{i<=n} while (i < n ) do i := i+1 {i=n}
Xem I là ( i <= n ) thì :
{ I and ( i < n )} i := i+1 {I} (a) // dễ kiểm chứng
Nên {I} while ( i < n ) do i := i+1 { I and not(i<n)} (b) // luật 3.3

Trần Hoàng Thọ Khoa Toán - Tin

Kỹ thuật lập trình nâng cao - 64 -
Mà I and not(i<n) (i <= n) and ( i >= n ) ==> i=n (c)
≡
Từ b ,c , luật hệ qủa ta có ĐPCM.

) }
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

) and ( t = x
o
) } (g) // d ,e, luật hệ
quả

Trần Hoàng Thọ Khoa Toán - Tin