程序正确性证明.ppt

程序正确性证明
第1页，本讲稿共55页
程序正确性概述
什么样的程序才是正确的？
如何来保证程序是正确的？
第2页，本讲稿共55页
关于程序正确性的认识
什么样的程序才是正确的？
Floyd的不变式断言法
B. Manna的子目标断言法
C. Hoare的公理化方法
终止性证明的方法
A. Floyd的良序集方法
B. Knuth的计数器方法

完全正确性的方法
A. Hoare公理化方法的推广
B. Burstall的间发断言法
C. Dijkstra的弱谓词变换方法以及强验证方法
第13页，本讲稿共55页
第5章 程序正确性证明



－－计数器法
第14页，本讲稿共55页
循环不变式断言
把反映循环变量的变化规律，且在每次循环体的执行前后均为真的逻辑表达式称为该循环的不变式断言。
例 带余整数除法问题：设x为非负整数，y为正整数，求 x除以y的商q，以及余数r。
程序：
q＝0；r＝x；
while( r ≥ y) //该循环不变式断言：
{
r ＝ r－y；
q ＝ q＋1；
}
//(x＝y×q＋r )∧ r ≥ 0
第15页，本讲稿共55页
不变式断言法
证明步骤：
1、建立断言
建立程序的输入、输出断言，如果程序中有循环出现的话，在循环中选取一个断点，在断点处建立一个循环不变式断言。
2、建立检验条件
将程序分解为不同的通路，为每一个通路建立一个检验条件，该检验条件为如下形式：
I ∧ R => O
其中I为输入断言，R为进入通路的条件，O为输出断言。
3、证明检验条件
运用数学工具证明步骤2得到的所有检验条件，如果每一条通路检验条件都为真，则该程序为部分正确的。
第16页，本讲稿共55页
不变式断言法实例1
例：设x,y为正整数，求x,y的最大公约数z的程序，即z=gcd(x,y)。
Function gcd(x1,x2:integer);
var y1,y2,z : Integer;
Begin
y1:=x1;y2:=x2;
while (y1<>y2) do
if (y1>y2)
y1:=y1-y2
else
y2:=y2-y1
z:=y1;
write(z);
End.
START
(x1,x2)－>(y1,y2)
y1<>y2
y1>y2
y1:=y1-y2
y2:=y2-y1
z:=y1
STOP
T
F
T
F
第17页，本讲稿共55页
不变式断言法实例1(建立断言)
输入断言：
I(x1,x2): x1>0 ∧x2>0
输出断言：
O(x1,x2,z):z=gcd(x1,x2)
循环不变式断言：
P(x1,x2,y1,y2):
x1>0 ∧ x2>0 ∧
y1>0 ∧ y2>0 ∧
gcd(y1,y2)=gcd(x1,x2)
通路划分：
通路1：a->b
通路2：b->d->b
通路3：b->e->b
通路4：b->g->c
START
(x1,x2)->(y1,y2)
y1<>y2
y1>y2
y1:=y1-y2
y2:=y2-y1
z:=y1
STOP
T
F
T
F
I(x1,x2)
a
P(x1,x2,y1,y2)
b
c
O(x1,x2,z)
d
e
g
·
·
·
·
·
·
第18页，本讲稿共55页
不变式断言法实例1(建立检验条件)
检验条件： I ∧ R => O
通路1：
I(x1,x2)=> P(x1,x2,y1,y2)
x1>0 ∧ x2>0 =>
x1>0∧ x2>0 ∧ y1>0 ∧Y2>0 ∧ gcd(y1,y2)=gcd(x1,x2)
通路2：
P(x1,x2,y1,y2) ∧ y1<>y2 ∧ y1>y2 => P(x1,x2