程序正确性证明

程序正确性证明第1页，共55页，2023年，2月20日，星期二5.1程序正确性概述什么样的程序才是正确的？如何来保证程序是正确的？第2页，共55页，2023年，2月20日，星期二关于程序正确性的认识什么样的程序才是正确的？

“测试”或“调试”方法

根据问题的特性和软件所要实现的功能，选择一些具有代表性的数据，设计测试用例。通过用例程序执行，去发现被测试程序的错误。

采用“测试”方法可以发现程序中的错误，但却不能证明程序中没有错误！因此，为保证程序的正确性，必须从理论上研究有关“程序正确性证明”的方法。第3页，共55页，2023年，2月20日，星期二程序正确性证明发展历程20世纪50年代Turing开始研究。1967年，Floyd和Naur提出不变式断言法。1969年，Hoare提出公理化方法。1975年，Dijkstra提出最弱前置谓词和程序推导方法，解决了断言构造难的问题，可从程序规约推导出正确程序，使正确性证明变得实用。

程序正确性理论是十分活跃的课题，不仅可以证明顺序程序的正确性，而且还可以证明非确定性程序，以及并行程序的正确性。第4页，共55页，2023年，2月20日，星期二程序正确性理论程序设计的一般过程第5页，共55页，2023年，2月20日，星期二程序正确性理论程序功能的精确描述1、程序规约：对程序所实现功能的精确描述，由程序的前置断言和后置断言两部分组成。2、前置断言：程序执行前的输入应满足的条件，又称为输入断言。3、后置断言：程序执行后的输出应满足的条件，又称为输出断言。程序设计过程：问题程序规约程序第6页，共55页，2023年，2月20日，星期二程序规约的基本分类非形式化程序规约非形式化程序规约采用自然语言描述程序功能，简单、方便，但存在二义性，因此，不利于程序的正确性证明。形式化程序规约采用数学化的语言描述程序功能，描述精确，无二义性，便于程序的正确性证明。第7页，共55页，2023年，2月20日，星期二程序规约的实例在书写程序规约时，使用Q表示前置断言，R表示后置断言，S表示问题求解的实现程序。在前置断言Q之前，还必须给出Q和R中所出现的标识符的必要说明。例1：求数组b[0:n-1]中所有元素的最大值。[inn:integer;inb[0:n-1]:arrayofinteger;outy:integer]Q:{n≥1}SR:{y＝MAX(i:0≤i＜n;b[i])}第8页，共55页，2023年，2月20日，星期二程序规约的实例例2：求两个非负整数的最大公约数。[ina,b:integer;outy:integer]Q:{a≥0∧b≥0}SR:{y＝MAX(i:1≤i≤min(a,b)∧(amodi＝0)∧(bmodi＝0))}第9页，共55页，2023年，2月20日，星期二程序正确性定义衡量一个程序的正确性，主要看程序是否实现了问题所要求的功能。若程序实现了问题所要求的功能，则称它为正确的，否则是不正确的。对程序的正确性理解，可以分为两个层次：从广义来说，一个程序的正确性取决于该程序满足问题实际需求的程度。从狭义而言，如果一个程序满足了它的程序规约就是正确的。程序设计过程：问题程序规约程序第10页，共55页，2023年，2月20日，星期二程序正确性定义程序规约Q{S}R是一个逻辑表达式，其取值为真或假。 其中取值为真的含义是指：给定一段程序S，若程序开始执行之前Q为真，S的执行将终止，且终止时R为真，则称为“程序S，关于前置断言Q和后置断言R是完全正确的”。第11页，共55页，2023年，2月20日，星期二程序正确性定义部分正确： 若对于每个使得Q(i)为真，并且程序S计算终止的输入信息i，R(i,S(i))都为真，则称程序S关于Q和R是部分正确的。程序终止： 若对于每个使得Q(i)为真的输入i，程序S的计算都终止，则称程序S关于Q是终止的。完全正确： 若对于每个使得Q(i)为真的输入信息i，程序S的计算都将终止，并且R(i,S(i))都为真，则称程序S关于Q和R是完全正确的。一个程序的完全正确，等价于该程序是部分正确，同时又是终止的。第12页，共55页，2023年，2月20日，星期二程序正确性的证明方法分类证明部分正确性的方法

A.Floyd的不变式断言法

B.Manna的子目标断言法

C.Hoare的公理化方法终止性证明的方法

A.Floyd的良序集方法

B.Knuth的计数器方法

C.Manna等人的不动点方法完全正确性的方法

A.Hoare公理化方法的推广

B.Burstall的间发断言法

C.Dijkstra的弱谓词变换方法以及强验证方法第13页，共55页，2023年，2月20日，星期二第5章程序正确性证明5.1程序正确性验证概述5.2不变式断言法5.3子目标断言法5.4界函数法－－计数器法第14页，共55页，2023年，2月20日，星期二循环不变式断言把反映循环变量的变化规律，且在每次循环体的执行前后均为真的逻辑表达式称为该循环的不变式断言。

例带余整数除法问题：设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页，2023年，2月20日，星期二5.2不变式断言法证明步骤：1、建立断言 建立程序的输入、输出断言，如果程序中有循环出现的话，在循环中选取一个断点，在断点处建立一个循环不变式断言。2、建立检验条件 将程序分解为不同的通路，为每一个通路建立一个检验条件，该检验条件为如下形式：

I∧R=>O

其中I为输入断言，R为进入通路的条件，O为输出断言。3、证明检验条件 运用数学工具证明步骤2得到的所有检验条件，如果每一条通路检验条件都为真，则该程序为部分正确的。第16页，共55页，2023年，2月20日，星期二不变式断言法实例1例：设x,y为正整数，求x,y的最大公约数z的程序，即z=gcd(x,y)。Functiongcd(x1,x2:integer);vary1,y2,z:Integer;Begin y1:=x1;y2:=x2; while(y1<>y2)do if(y1>y2)y1:=y1-y2elsey2:=y2-y1z:=y1;write(z);End.START(x1,x2)－>(y1,y2)y1<>y2y1>y2y1:=y1-y2y2:=y2-y1z:=y1STOPTFTF第17页，共55页，2023年，2月20日，星期二不变式断言法实例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->cSTART(x1,x2)->(y1,y2)y1<>y2y1>y2y1:=y1-y2y2:=y2-y1z:=y1STOPTFTFI(x1,x2)aP(x1,x2,y1,y2)bcO(x1,x2,z)deg······第18页，共55页，2023年，2月20日，星期二不变式断言法实例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,y1-y2,y2)x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)∧y1<>y2∧y1>y2=>x1>0∧x2>0∧y1-y2>0∧y2>0∧gcd(y1-y2,y2)=gcd(x1,x2)第19页，共55页，2023年，2月20日，星期二不变式断言法实例1(建立检验条件)通路3：P(x1,x2,y1,y2)∧y1<>y2∧y1<y2=>P(x1,x2,y1,y2-y1)x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)∧y1<>y2∧y1<y2=>x1>0∧x2>0∧y1>0∧y2-y1>0∧gcd(y1,y2-y1)=gcd(x1,x2)通路4：P(x1,x2,y1,y2)∧y1=y2=>O(x1,x2,z)x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)∧y1=y2=>z=gcd(x1,x2)第20页，共55页，2023年，2月20日，星期二不变式断言法实例1(证明检验条件)通路1：

x1>0∧x2>0∧x1=y1∧x2=y2=>……通路2：

若y1>y2,gcd(y1-y2,y2)=gcd(y1,y2)=gcd(x1,x2)通路3:

若y2>y1,gcd(y1,y2)=gcd(y1,y2-y1)=gcd(x1,x2)通路4:

若y1=y2,gcd(y1,y2)=gcd(x1,x2)=y1=y2=zP(x1,x2,y1,y2)∧y1=y2=>O(x1,x2,z)第21页，共55页，2023年，2月20日，星期二不变式断言法实例2对任一给定的自然数x，计算z＝[]，即计算x的平方根取整。1＋3＋…(2n+1)=(n+1)2y1=n;y3=2×y1+1;y2=(y1+1)2输入断言：

I(x):x>0输出断言：

O(x,z):z2≤x<(z+1)2循环不变式：

P(x,y1,y2,y3)：

y12≤x∧y2=(y1+1)2

∧y3=2y1+1开始(0,0,1)－>(y1,y2,y3)y2+y3－>y2y2≤x(y1+1,y3+2)－>(y1,y3)y1－>z结束AI(x)BP(x,y1,y2,y3)DCO(x,z)FT····第22页，共55页，2023年，2月20日，星期二不变式断言法实例2检验条件：I∧R=>O通路1：A->BI(x)=>P(x,0,1,1)x>0=>0≤x∧1=(0+1)2∧1=2*0+1通路2：B->D->BP(x,y1,y2,y3)∧y2≤x=>p(x,y1+1,y2+y3+2,y3+2)y12≤x∧y2=(y1+1)2∧y3=2y1+1∧y2≤x=>(y1+1)2≤x∧y2+y3+2=(y1+1+1)2∧y3+2=2(y1+1)+1通路3：B->CP(x,y1,y2,y3)∧y2>x=>O(x,y1)y12≤x∧y2=(y1+1)2∧y3=2y1+1∧y2>x=>

y12≤x<(y1+1)2第23页，共55页，2023年，2月20日，星期二不变式断言法实例2检验条件2y12≤x∧y2=(y1+1)2∧y3=2y1+1∧y2≤x=>(y1+1)2≤x∧y2+y3+2=(y1+1+1)2∧y3+2=2(y1+1)+1证明：x≥(y1+1)2——(y2≤x,y2=(y1+1)2

)y2+y3+2=(y1+1)2+2y1+1+2 =(y1+1)2+2(y1+1)+1=(y1+1+1)2y3+2=2y1+1+2=2(y1+1)+1检验条件3y12≤x∧y2=(y1+1)2∧y3=2y1+1∧y2>x=>y12≤x<(y1+1)2

证明：

y12≤xx<y2,y2=(y1+1)2=>x<(y1+1)2第24页，共55页，2023年，2月20日，星期二作业课本P174习题1、习题2。要求用不变式断言法证明。第25页，共55页，2023年，2月20日，星期二第5章程序正确性证明5.1程序正确性验证概述5.2不变式断言法5.3子目标断言法5.4界函数法－－计数器法第26页，共55页，2023年，2月20日，星期二5.3子目标断言法子目标断言法与不变式断言法的主要区别是：两种方法对循环所建立的断言不同。不变式断言描述了程序变量y的中间值与初始值之间关系；子目标断言法描述的是y的中间值与循环终止时的最终值yend之间的关系。两种方法进行归纳的方向不同。不变式断言沿着程序正常执行的方向进行归纳；子目标断言法则沿着相反方向进行归纳。第27页，共55页，2023年，2月20日，星期二不变式断言法输入断言：

I(x,y):x0>=0∧y0>=0输出断言：

O(x,y,z):z=gcd(x,y)循环不变式断言：P(x,y):x>=0∧y>=0∧ gcd(x,y)=gcd(x0,y0)例：设x,y为非负整数，求x,y的最大公约数z的程序，即z=gcd(x,y)。STARTRead(x,y)x<>0y>=xy:=y-xxyz:=ySTOPTFTFI(x,y)aP(x,y)bcO(x,y,z)deg······第28页，共55页，2023年，2月20日，星期二子目标断言法(建立断言)输入断言

I(x,y):x0>=0∧

y0>=0∧(x0≠0∨y0≠0)输出断言

O(x,y,z):z=gcd(x,y)子目标断言

P(x,y,yend):x>=0∧y>=0∧(x≠0∨y≠0)

=>yend=gcd(x,y)STARTRead(x,y)x<>0y>=xy:=y-xxyz:=ySTOPTFTFI(x,y)aP(x,y,yend)bcO(x,y,z)deg······第29页，共55页，2023年，2月20日，星期二子目标断言法(建立检验条件)通路1： 控制转出循环时，子目标断言成立。通路2、通路3： 如果在通过循环之后，子目标断言在断点处成立，那么，在通过循环之前，断言也成立。通路4： 如果输入断言为真，且控制第一次通过断点B时子目标断言为真，则输出断言为真。第30页，共55页，2023年，2月20日，星期二子目标断言法(建立检验条件)通路1：b->c检验条件1 x=0=>P(x,y,yend)x=0=>

[x>=0∧y>=0∧

(x≠0∨y≠0)

=> yend=gcd(x,y)]

通路2：b->d->b检验条件2P(x,y-x,yend)∧x<>0∧y>=x=>P(x,y,yend)[x>=0∧y-x>=0∧

(x≠0∨y-x≠0)

=>yend=gcd(x,y-x)]∧x<>0∧y>=x=>

[x>=0∧y>=0∧(x≠0∨y≠0)

=>yend=gcd(x,y)]通路3：b->e->b检验条件3P(y,x,yend)∧x<>0∧y<x=>P(x,y,yend)通路4：a->b检验条件4x0>=0∧

y0>=0∧

(x0≠0∨y0

≠0)

∧P(x0,y0,yend)=>yend=gcd(x0,y0)第31页，共55页，2023年，2月20日，星期二子目标断言法(证明检验条件)检验条件1：

x=0=>[x>=0∧y>=0=>yend=gcd(x,y)]证明： 因为有x=0,yend=y

所以yend=y=gcd(0,y)=gcd(x,y)检验条件2：P(x,y-x,yend)∧x<>0∧y>x=>P(x,y,yend)即证明：[x>=0∧y-x>=0∧(x≠0∨y-x≠0)=>

yend=gcd(x,y-x)]∧x<>0∧y>=x=>

[x>=0∧y>=0∧(x≠0∨y≠0)=>

yend=gcd(x,y)]

第32页，共55页，2023年，2月20日，星期二程序部分正确但不终止实例例：求两个非负整数x、y的最大公约数z的程序。ProgramAvarx,y,z,s:integer;beginread(x,y);whilex≠0doify>xtheny=y–x;elsex=x–y;z=y;write(z);end.STARTRead(x,y)x≠0y>xy:=y-xx:=x-yz:=ySTOPTFTFI(x,y)aP(x,y)bcO(x,y,z)deg······可以利用不变式断言等方法证明该程序的部分正确性，但无法证明它是终止的。因为当y＝0时，程序循环将不终止！

第33页，共55页，2023年，2月20日，星期二第5章程序正确性证明5.1程序正确性验证概述5.2不变式断言法5.3子目标断言法5.4界函数法－－计数器法第34页，共55页，2023年，2月20日，星期二5.5良序集方法证明程序终止性1.基本概念偏序集良序集2.采用良序集方法证明程序终止性第35页，共55页，2023年，2月20日，星期二偏序集的概念偏序集 设有一个非空集合W和一个定义在W上的二元关系

，且这个关系满足下列性质：1）传递性，即对于一切a,b,c∈W,如果a

b,b

c，则a

c2）反对称性，即对于a

b,则有b≮a3）反自反性，即对于一切a∈W，a≮a

称W为具有关系的偏序集，记做（W,）。例如：（1）具有小于关系（<）的，位于0～1之间的实数集合A1。（2）具有小于关系（<）的全体整数集合B1。但将<换成≤就不是偏序集。（1）具有小于等于关系（≤）的，位于0～1之间的实数集合A1。（2）具有小于等于关系（≤）的全体整数集合B1。第36页，共55页，2023年，2月20日，星期二良序集的概念良序集 设（W,）是偏序集，如果不存在由W中的元素构成的无限递减序列:……a2

a1

a0，则称（W,）是良序集。 例如：（1）若N是自然数集合，那么（N，<）是良序集。（2）具有通常序A

B

C…

Z的字母表∑={A,B,…,Z}是良序集。 下述集合A1和B1是偏序集，但不是良序集。（1）具有小于关系（<）的，位于0～1之间的实数集合A1。（2）具有小于关系（<）的全体整数集合B1。第37页，共55页，2023年，2月20日，星期二采用良序集证明程序终止性思路结构化程序由顺序、选择和循环三种基本结构组成，而影响程序终止性的是循环结构，因此，是程序终止性证明的重点。程序终止性证明思路：

A.选取良序集合（W,）；

B.选取割点集，割断循环；

C.在割点上寻找函数u，使u∈W；

D.证明每次循环，u依次递减。 由于良序集合（W,）不存在无穷递减序列，因此，循环必然终止。第38页，共55页，2023年，2月20日，星期二用良序集方法证明程序终止性步骤1.选取一个点集去截断程序的各个循环部分，并在每个截断点i处建立中间断言Qi(x,y)；2.选取一个良序集(W,

)，并在每个截断点处定义一个终止表达式Ei(x,y)，表达式在W上取值；3.证明对每一个从程序入口到截断点j的通路aj有

I(x)∧Raj

(x,y)=>Qj(x,raj(x,y))

证明对每一个从截断点i到截断点j的通路aij

，有

Qi(x,y)∧Raij(x,y)=>Qj(x,raij(x,y))

即证明中间断言是“正确的”，是“良断言”；4.证明Qi(x,y)=>Ei(x,y)∈W，即终止表达式是良函数；5.证明对于每一个从截断点i到截断点j的通路aij

，有

Qi(x,y)∧Raj(x,y)=>[Ej(x,y)

Ei(x,y)]。第39页，共55页，2023年，2月20日，星期二良序集方法证明程序终止性实例例子：对任一给定的自然数x，计算z＝[]，即计算x的平方根取整。开始(0,0,1)－>(y1,y2,y3)y2+y3－>y2y2＞

x(y1+1,y3+2)－>(y1,y3)y1－>z结束B’·TF第40页，共55页，2023年，2月20日，星期二良序集方法证明程序终止性实例1.选取断点B’

，建立中间断言

Q(x,y1,y2,y3):y2<x∧y3>02.取良序集（N,<），其中N为自然数集合，在B’建立终止表达式：

E(x,y1,y2,y3):x-y23.证明Q(x,y1,y2,y3)是良断言从程序开始点->B’

：I(x)=>Q(x,y1,y2,y3)，即：x>0=>[0<x∧1>0]

从截断点B’->B’：

Q(x,y1,y2,y3)∧y2+y3<x=> Q(x,y1+1,y2+y3,y3+2)

即：[y2<x∧y3>0∧y2+y3<x]=>[y2+y3<x∧y3+2>0]第41页，共55页，2023年，2月20日，星期二良序集方法证明程序终止性实例4.证明E(x,y)是良函数，即证明Q(x,y)=>E(x,y)∈N，即

[y2<x∧y3>0]=>x-y2>0∈N5.证明终止条件成立

[Q(x,y)∧y2+y3<x]=>[E(x,y1+1,y2+y3,y3+2)<E(x,y1,y2,y3)]

即：

[y2<x∧y3>0∧y2+y3<x]=>[x-y2-y3<x-y2]第42页，共55页，2023年，2月20日，星期二采用良序集证明程序终止性总结1、采用良序集方法证明程序终止性，关键在于选择合适的中间断言Qi(x,y)和终止表达式Ei(x,y)。2、采用良序集证明程序终止性，与程序部分正确性证明采用了不同途径，相互完全独立，因此，证明程序的完全正确性工作量较大。3、采用计数器方法可以将程序的部分正确性和终止性证明结合进行。第43页，共55页，2023年，2月20日，星期二5.6计数器方法证明程序终止性证明思路 通过估计循环执行的最大次数证明程序终止性的方法。证明步骤:1.为程序的每一个循环附加一个新的变量作为该循环的计数器，初始值置为0，每循环一次该计数器加1。2.为每个循环设置一个中间断言，它表示相应的计数器不会超过固定的界限。3.证明（2）中的中间断言是不变式断言。第44页，共55页，2023年，2月20日，星期二计数器方法证明程序终止性实例计算非负整数的最大公约数varx,y,z,s:integer;beginRead(x,y)whilex≠0dobeginIfy≥xthen y:=y-x;else s:=x;x:=y;y:=s;endz:=y;write(z);endSTARTRead(x,y)x≠0y≥xy:=y-xxyz:=ySTOPTFTFI(x,y)aP(x,y)bO(x,y)de····c·第45页，共55页，2023年，2月20日，星期二计数器方法证明程序终止性实例1.引进计数器I,并建立如下断言

x≥0∧y≥0∧2x+y+I≤2x0+y0

varx,y,z,s:integer;read(x,y);I:=0;//计数器赋初值whilex≠0dobeginify≥xtheny:=y-x; elses:=x;x:=y;y:=sfi;I:=I+1;//计数器递增End;z:=y;write(z);第46页，共55页，2023年，2月20日，星期二计数器方法证明程序终止性实例2.建立检验条件并证明，从而证明计数器断言为不变式断言。检验条件1：a->b [x0≥0∧y0≥0]=>[x0≥0∧y0≥0∧2x0+y0+0≤2x0+y0]检验条件2：b->d->b[x≥0∧y≥0∧(2x+y+I≤2x0+y0)∧x≠0∧y≥x]=>[x≥0∧y-x≥0∧(2x+(y-x)+I+1≤2x0+y0)]证明：x≠0=>(x-1≥0)

∴2x+(y-x)+I+1=2x+y+I-(x-1)≤2x+y+I≤2x0+y0检验条件3：b->e->b[x≥0∧y≥0∧(2x+y+I≤2x0+y0)∧x≠0∧y<x]=>[y≥0∧x≥0∧(2y+x+I+1≤2x0+y0)]证明：(y<x∧x≠0=>y≤x-1)

∴2y+x+I+1≤y+x-1+x+I+1=y+2x+I≤2x0+y0由于2x+y+I≤2x0+y0是不变式断言，因此，I（循环次数）必定小于常量2x0+y0

，也就是循环只能执行有限次，即程序终止。采用计数器方法证明程序终止性和利用不变式断言法证明部分正确性步骤完全类似，只要再添加输出断言部分检验条件并证明，即可完成程序部分正确性证明。因此，可以把上述两者联合起来，完成程序的完全正确性证明。

第47页，共55页，2023年，2月20日，星期二5.4界函数法－－证明程序的可终止性该方法是计数器方法的一种变形，证明程序的可终止性的常用方法.界函数法:对程序中的每一个循环,构造一个界函数,若该循环存在界函数,则该循环是可终止的,否则,该循环不可终止.界函数必须满足的条件:(1)与循环变量有关的整函数,记为N(x,y);(2)在循环的过程中N(x,y)>0;