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.

.

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?

3 . Tiên đề rẽ nhánh

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à A,!E=>B 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}

ii. {A,!E: x,y,q,r∈N, x=qy+r, 0≤ r<2y, y>r}=>{BL }

do đó suy ra {A}P{B}.

4 . Tính bất biến của c hươ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}.

5 . 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 doP; {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

End;

Return z;

If (x mod 2)≠0 then z:=z+y;

x=x div 2;

y:=y*2;

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à

Lii..{C,E,!F: x,y,z∈N; ab=z+xy;x>0,(x mod 2)=0} =>{C2};

Vậy {C} là bất biến của Q. Nên kết thúc Q, ta có mệnh đề {C,!E}.

L

+ 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}.