24/05/2018, 19:13

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. Như ta đã biết, chương trình P là một bộ biến đổi tuần tự P để chuyển cái vào x thành ra ...

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.

Như ta đã biết, chương trình P là một bộ biến đổi tuần tự P để chuyển cái vào x thành ra cái y; ở đây x và y hoàn toàn được xác định trước.

Như vậy, một chương trình P được gọi là đúng nếu nó thực hiện chính xác những mục tiêu do người thiết kế đặc ra. Ta gọi:

+ Giả thiết A là mệnh đề được phát biểu để thể hiện tính chất của cái vào, gọi tắt là mệnh đề dữ liệu vào.

+ Kết luận B là mệnh đề được phát biểu để tính chất cần có của dữ liệu ra, gọi tắt là mệnh đề dữ liệu ra.

1 . Tiên đề 1: Tiên đề tuần tự

Nếu mệnh đề A sau khi chịu tác động của khối cấu trúc điều khiển P ta được

B và mệnh đề B sau khi chịu tác động của cấu trúc điều khiển Q ta được C thì

A chịu tác động tuần tự P,Q sẽ thu được C

Hay nói cách khác, đây chính là tiên đề về dãy thao tác: Nếu A P B và B

Q C thì A P,Q C

2 . Tiên đề gán: tính chất của phép gán

Điều kiện để có mệnh đề B sau khi thực hiện lệnh gán x: = E (với E là một biểu thức) từ mệnh đề {A} thì trước đó ta phải có {A} suy dẫn được ra {B[x|E]}.

Kỹ thuật lần ngược của tiên đềgán

.

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

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

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

0