程序正确性证明概述课件

第5章程序正确性证明5.1程序正确性验证概述5.2不变式断言法5.3子目标断言法5.4界函数法－－计数器法第5章程序正确性证明5.1程序正确性验证概述15.1程序正确性概述什么样的程序才是正确的？如何来保证程序是正确的？5.1程序正确性概述什么样的程序才是正确的？2计算机程序是算法的一种精确描述，算法的任务是把给定的输入信息变换为所需要的输出信息。所谓一段程序是正确的，是指这段程序能准确无误地完成编写者所期望赋予它的功能。或者说，对任何一组允许的输入信息，程序执行后能得到一组和这组输入信息相对应的正确的输出信息。通俗地说，“做了它该做的事，没有做它不该做的事”。结构化程序的正确性验证计算机程序是算法的一种精确描述，算法的任务是把给定的输入信息3一段程序是错误的，是指：(1)程序完成的事情并不是程序员想要完成的事情；(2)程序员想要程序完成的事情，程序并没有完成。一般来说，程序中含有错误是很难避免的错误可能有：（1）设计时的错误；（2）程序编写时的错误；（3）运行时的错误等;……一段程序是错误的，是指：4如何发现错误或尽量减少错误？(1)设计程序时尽可能使用结构化程序设计方法，使程序设计过程规范化和标准化；(2)程序调试或运行时采用测试的方法去跟踪程序的运行，从而发现与改正错误；(3)利用程序正确性证明的方法检验程序是否正确。如何发现错误或尽量减少错误？51983年IEEE提出的软件工程术语中给软件测试下的定义是：“使用人工或者自动手段来运行或测定某个系统的过程，其目的在于检验它是否满足规定的需求或是弄清预期结果与实际结果之间的差别。”测试是程序的执行过程，目的在于发现错误。一个好的测试用例在于能发现至今未发现的错误；一个成功的测试是发现了至今未发现的错误的测试。1983年IEEE提出的软件工程术语中给软件测试下的定义是：6测试的原则1.应当“尽早地和不断地进行软件测试”。2.测试用例应由测试输入数据和对应的预期输出结果组成。3.程序员应避免检查自己的程序。4.在设计测试用例时，应当包括合理的输入条件和不合理的输入条件。测试的原则1.应当“尽早地和不断地进行软件测试”。75.充分注意测试中的群集现象。即测试后程序中残存的错误数目与该程序中已发现的错误数目成正比。6.严格执行测试计划，排除测试的随意性。7.应当对每一个测试结果做全面检查。8.妥善保存测试计划，测试用例，出错统计和最终分析报告，为维护提供方便。5.充分注意测试中的群集现象。即测试后程序中残存的错误数目8程序测试实质上只是一种抽样检查测试过程：选取测试数据→执行程序→输入测试数据→记录执行结果→手工核对结果因此，测试只是一种查错的手段，它可以帮助人们去发现程序中的错误，但不能证明程序中没有错误，即：测试不能证明程序是正确的程序测试实质上只是一种抽样检查9测试只能发现程序错误，但不能证明程序无错。原因：测试并没有也不可能包含所有数据，只是选择了一些具有代表性的数据，所以它具有局限性。正确性证明是通过数学技术来确定软件是否正确，也就是说，是否符合其规格说明。测试只能发现程序错误，但不能证明程序无错。10关于程序正确性的认识什么样的程序才是正确的？

“测试”或“调试”方法

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

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

程序正确性理论是十分活跃的课题，不仅可以证明顺序程序的正确性，而且还可以证明非确定性程序，以及并行程序的正确性。程序正确性证明发展历程20世纪50年代Turing开始研究12程序正确性理论程序设计的一般过程程序正确性理论程序设计的一般过程13程序正确性理论程序功能的精确描述1、程序规约：对程序所实现功能的精确描述，由程序的前置断言和后置断言两部分组成。2、前置断言：程序执行前的输入应满足的条件，又称为输入断言。3、后置断言：程序执行后的输出应满足的条件，又称为输出断言。程序设计过程：问题程序规约程序程序正确性理论程序功能的精确描述程序设计过程：问题14程序规约的基本分类非形式化程序规约非形式化程序规约采用自然语言描述程序功能，简单、方便，但存在二义性，因此，不利于程序的正确性证明。形式化程序规约采用数学化的语言描述程序功能，描述精确，无二义性，便于程序的正确性证明。程序规约的基本分类非形式化程序规约15程序规约的实例在书写程序规约时，使用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])}程序规约的实例在书写程序规约时，使用Q表示前置断言，R表示后16程序规约的实例例2：求两个非负整数的最大公约数。[ina,b:integer;outy:integer]Q:{a≥0∧b≥0}SR:{y＝MAX(i:1≤i≤min(a,b)∧(amodi＝0)∧(bmodi＝0))}程序规约的实例例2：求两个非负整数的最大公约数。17程序正确性定义衡量一个程序的正确性，主要看程序是否实现了问题所要求的功能。若程序实现了问题所要求的功能，则称它为正确的，否则是不正确的。对程序的正确性理解，可以分为两个层次：从广义来说，一个程序的正确性取决于该程序满足问题实际需求的程度。从狭义而言，如果一个程序满足了它的程序规约就是正确的。程序设计过程：问题程序规约程序程序正确性定义衡量一个程序的正确性，主要看程序是否实现了问题18程序正确性定义程序规约Q{S}R是一个逻辑表达式，其取值为真或假。 其中取值为真的含义是指：给定一段程序S，若程序开始执行之前Q为真，S的执行将终止，且终止时R为真，则称为“程序S，关于前置断言Q和后置断言R是完全正确的”。程序正确性定义程序规约Q{S}R是一个逻辑表达式，其取值为真19程序正确性定义部分正确： 若对于每个使得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是完全正确的。一个程序的完全正确，等价于该程序是部分正确，同时又是终止的。程序正确性定义部分正确：20程序正确性的证明方法分类证明部分正确性的方法

A.Floyd的不变式断言法

B.Manna的子目标断言法

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

A.Floyd的良序集方法

B.Knuth的计数器方法

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

A.Hoare公理化方法的推广

B.Burstall的间发断言法

C.Dijkstra的弱谓词变换方法以及强验证方法程序正确性的证明方法分类证明部分正确性的方法21第5章程序正确性证明5.1程序正确性验证概述5.2不变式断言法5.3子目标断言法5.4界函数法－－计数器法第5章程序正确性证明5.1程序正确性验证概述22循环不变式断言把反映循环变量的变化规律，且在每次循环体的执行前后均为真的逻辑表达式称为该循环的不变式断言。

例带余整数除法问题：设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循环不变式断言把反映循环变量的变化规律，且在每次循环体的执行235.2不变式断言法证明步骤：1、建立断言 建立程序的输入、输出断言，如果程序中有循环出现的话，在循环中选取一个断点，在断点处建立一个循环不变式断言。2、建立检验条件 将程序分解为不同的通路，为每一个通路建立一个检验条件，该检验条件为如下形式：

I∧R=>O

其中I为输入断言，R为进入通路的条件，O为输出断言。3、证明检验条件 运用数学工具证明步骤2得到的所有检验条件，如果每一条通路检验条件都为真，则该程序为部分正确的。5.2不变式断言法证明步骤：24不变式断言法实例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不变式断言法实例1例：设x,y为正整数，求x,y的最大公约数25不变式断言法实例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······不变式断言法实例1(建立断言)输入断言：通路划分：ST26不变式断言法实例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)不变式断言法实例1(建立检验条件)检验条件：I∧R=27不变式断言法实例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)不变式断言法实例1(建立检验条件)通路3：28不变式断言法实例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)不变式断言法实例1(证明检验条件)通路1：29不变式断言法实例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····不变式断言法实例2对任一给定的自然数x，计算z＝[30不变式断言法实例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不变式断言法实例2检验条件：I∧R=>O31不变式断言法实例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不变式断言法实例2检验条件232作业课本P174习题1、习题2。要求用不变式断言法证明。作业课本P174习题1、习题2。要求用不变式断言法证明。33第5章程序正确性证明5.1程序正确性验证概述5.2不变式断言法5.3子目标断言法5.4界函数法－－计数器法第5章程序正确性证明5.1程序正确性验证概述345.3子目标断言法子目标断言法与不变式断言法的主要区别是：两种方法对循环所建立的断言不同。不变式断言描述了程序变量y的中间值与初始值之间关系；子目标断言法描述的是y的中间值与循环终止时的最终值yend之间的关系。两种方法进行归纳的方向不同。不变式断言沿着程序正常执行的方向进行归纳；子目标断言法则沿着相反方向进行归纳。5.3子目标断言法子目标断言法与不变式断言法的主要区别是：35不变式断言法输入断言： 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······不变式断言法输入断言：例：设x,y为非负整数，求x,y的最大36子目标断言法(建立断言)输入断言

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······子目标断言法(建立断言)输入断言STARTRe37子目标断言法(建立检验条件)通路1： 控制转出循环时，子目标断言成立。通路2、通路3： 如果在通过循环之后，子目标断言在断点处成立，那么，在通过循环之前，断言也成立。通路4： 如果输入断言为真，且控制第一次通过断点B时子目标断言为真，则输出断言为真。子目标断言法(建立检验条件)通路1：38子目标断言法(建立检验条件)通路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)子目标断言法(建立检验条件)通路1：b->c39子目标断言法(证明检验条件)检验条件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)]

子目标断言法(证明检验条件)检验条件1：40程序部分正确但不终止实例例：求两个非负整数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时，程序循环将不终止！

程序部分正确但不终止实例例：求两个非负整数x、y的最大公约数41第5章程序正确性证明5.1程序正确性验证概述5.2不变式断言法5.3子目标断言法5.4界函数法－－计数器法第5章程序正确性证明5.1程序正确性验证概述425.4计数器方法证明程序终止性证明思路 通过估计循环执行的最大次数证明程序终止性的方法。证明步骤:1.为程序的每一个循环附加一个新的变量作为该循环的计数器，初始值置为0，每循环一次该计数器加1。2.为每个循环设置一个中间断言，它表示相应的计数器不会超过固定的界限。3.证明（2）中的中间断言是不变式断言。5.4计数器方法证明程序终止性证明思路43计数器方法证明程序终止性实例计算非负整数的最大公约数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·计数器方法证明程序终止性实例计算非负整数的最大公约数var44计数器方法证明程序终止性实例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);计数器方法证明程序终止性实例1.引进计数器I,并建立如下断言45计数器方法证明程序终止性实例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，也就是循环只能执行有限次，即程序终止。采用计数器方法证明程序终止性和利用不变式断言法证明部分正确性步骤完全类似，只要再添加输出断言部分检验条件并证明，即可完成程序部分正确性证明。因此，可以把上述两者联合起来，完成程序的完全正确性证明。

计数器方法证明程序终止性实例2.建立检验条件并证明，从而证明465.4界函数法－－计数器方法的变形该方法是计数器方法的一种变形，证明程序的可终止性的常用方法.界函数法:对程序中的每一个循环,构造一个界函数,若该循环存在界函数,则该循环是可终止的,否则,该循环不可终止.界函数必须满足的条件:(1)与循环变量有关的整函数,记为N(x,y);(2)在循环的过程中N(x,y)>0;(3)每执行一次循环,N(x,y)的值减小.5.4界函数法－－计数器方法的变形该方法是计数器方法的一种473.4界函数法－－计数器法例3.证明例1的可终止性.y1:=x1,y2:=x2y1<>y2y1>y2z:=y1y2:=y2-y1y1:=y1-y2ABCDEFTFT取N(x,y)=max(y1,y2)3.4界函数法－－计数器法例3.证明例1的可终止性.y1:=483.4界函数法－－计数器法因为x1>0^x2>0,所以循环第一次进入循环时y1>0^y2>0.进入循环以后,当y1>y2时,y1=y1-y2>0,y2不变,所以N(x,y)>0.当y1<y2时,y2=y2-y1>0,y1不变,所以N(x,y)>0.故在循环过程中N(x,y)>0;当y1>y2时,N(y1-y2,y2)<N(y1,y2)当y1<y2时,N(y1,y2-y1)<N(y1,y2)故随着循环的执行,N(x,y)递减.故该循环存在界函数N(x,y)=max(y1,y2),所以该循环可终止.3.4界函数法－－计数器法因为x1>0^x2>0,所以循环第49另一种计数器方法证明程序终止性证明思路： 对程序中的每一个循环，构造一个和该循环中变量有关的整数函数N(x,y)，若N(x,y)满足以下两个条件：当循环条件成立时，N(x,y)>0；每次循环，N(x,y)都减小。 由N(x,y)的值构成一个单调递减的整数序列，N(x,y)>0，因而，循环只能执行有限次。另一种计数器方法证明程序终止性证明思路：50另一种计数器方法证明程序终止性实例例：设x,y为正整数，求x,y的最大公约数z的程序，即z=gcd(x,y)。START(x1,x2)－>(y1,y2)y1≠y2y1>y2y1:=y1－y2y2:=y2－y1z:=y1STOPTFTF另一种计数器方法证明程序终止性实例例：设x,y为正整数，求x51另一种计数器方法证明程序终止性实例选取N(y1,y2)=max(y1,y2)输入断言：

I(x1,x2):x1>0∧x2>0当第一次进入循环时有

y1>0∧y2>0有算法得y1>y2,则y1-y2－>y1,y2不变；y1<y2,则y2-y1－>y2,y1不变。∴始终有y1>0∧y2>0于是就有N(y1,y2)>0;每执行一次循环，N(y1,y2)是递减的。START(x1,x2)->(y1,y2)y1≠y2y1>y2y1:=y1-y2y2:=y2-y1z:=y1STOPTFTF另一种计数器方法证明程序终止性实例选取N(y1,y2)=52采用计数器方法证明程序终止性难点采用计数器方法证明程序终止性关键在于确定一个合适的中间断言（或选取一个合适的函数N（x,y）），尤其对于一些循环次数事先难以估计的程序，要找出循环次数的上限更为困难。采用计数器方法证明程序终止性难点采用计数器方法证明程序终止性53正整数的一个性质对于任意正整数，满足下列关系：若y1>y2,gcd(y1,y2)=gcd(y1-y2,y2)若y2>y1,gcd(y1,y2)=gcd(y1,y2-y1)若y1=y2,gcd(y1,y2)=y1=y2正整数的一个性质对于任意正整数，满足下列关系：54演讲完毕，谢谢观看！演讲完毕，谢谢观看！55第5章程序正确性证明5.1程序正确性验证概述5.2不变式断言法5.3子目标断言法5.4界函数法－－计数器法第5章程序正确性证明5.1程序正确性验证概述565.1程序正确性概述什么样的程序才是正确的？如何来保证程序是正确的？5.1程序正确性概述什么样的程序才是正确的？57计算机程序是算法的一种精确描述，算法的任务是把给定的输入信息变换为所需要的输出信息。所谓一段程序是正确的，是指这段程序能准确无误地完成编写者所期望赋予它的功能。或者说，对任何一组允许的输入信息，程序执行后能得到一组和这组输入信息相对应的正确的输出信息。通俗地说，“做了它该做的事，没有做它不该做的事”。结构化程序的正确性验证计算机程序是算法的一种精确描述，算法的任务是把给定的输入信息58一段程序是错误的，是指：(1)程序完成的事情并不是程序员想要完成的事情；(2)程序员想要程序完成的事情，程序并没有完成。一般来说，程序中含有错误是很难避免的错误可能有：（1）设计时的错误；（2）程序编写时的错误；（3）运行时的错误等;……一段程序是错误的，是指：59如何发现错误或尽量减少错误？(1)设计程序时尽可能使用结构化程序设计方法，使程序设计过程规范化和标准化；(2)程序调试或运行时采用测试的方法去跟踪程序的运行，从而发现与改正错误；(3)利用程序正确性证明的方法检验程序是否正确。如何发现错误或尽量减少错误？601983年IEEE提出的软件工程术语中给软件测试下的定义是：“使用人工或者自动手段来运行或测定某个系统的过程，其目的在于检验它是否满足规定的需求或是弄清预期结果与实际结果之间的差别。”测试是程序的执行过程，目的在于发现错误。一个好的测试用例在于能发现至今未发现的错误；一个成功的测试是发现了至今未发现的错误的测试。1983年IEEE提出的软件工程术语中给软件测试下的定义是：61测试的原则1.应当“尽早地和不断地进行软件测试”。2.测试用例应由测试输入数据和对应的预期输出结果组成。3.程序员应避免检查自己的程序。4.在设计测试用例时，应当包括合理的输入条件和不合理的输入条件。测试的原则1.应当“尽早地和不断地进行软件测试”。625.充分注意测试中的群集现象。即测试后程序中残存的错误数目与该程序中已发现的错误数目成正比。6.严格执行测试计划，排除测试的随意性。7.应当对每一个测试结果做全面检查。8.妥善保存测试计划，测试用例，出错统计和最终分析报告，为维护提供方便。5.充分注意测试中的群集现象。即测试后程序中残存的错误数目63程序测试实质上只是一种抽样检查测试过程：选取测试数据→执行程序→输入测试数据→记录执行结果→手工核对结果因此，测试只是一种查错的手段，它可以帮助人们去发现程序中的错误，但不能证明程序中没有错误，即：测试不能证明程序是正确的程序测试实质上只是一种抽样检查64测试只能发现程序错误，但不能证明程序无错。原因：测试并没有也不可能包含所有数据，只是选择了一些具有代表性的数据，所以它具有局限性。正确性证明是通过数学技术来确定软件是否正确，也就是说，是否符合其规格说明。测试只能发现程序错误，但不能证明程序无错。65关于程序正确性的认识什么样的程序才是正确的？

“测试”或“调试”方法

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

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

程序正确性理论是十分活跃的课题，不仅可以证明顺序程序的正确性，而且还可以证明非确定性程序，以及并行程序的正确性。程序正确性证明发展历程20世纪50年代Turing开始研究67程序正确性理论程序设计的一般过程程序正确性理论程序设计的一般过程68程序正确性理论程序功能的精确描述1、程序规约：对程序所实现功能的精确描述，由程序的前置断言和后置断言两部分组成。2、前置断言：程序执行前的输入应满足的条件，又称为输入断言。3、后置断言：程序执行后的输出应满足的条件，又称为输出断言。程序设计过程：问题程序规约程序程序正确性理论程序功能的精确描述程序设计过程：问题69程序规约的基本分类非形式化程序规约非形式化程序规约采用自然语言描述程序功能，简单、方便，但存在二义性，因此，不利于程序的正确性证明。形式化程序规约采用数学化的语言描述程序功能，描述精确，无二义性，便于程序的正确性证明。程序规约的基本分类非形式化程序规约70程序规约的实例在书写程序规约时，使用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])}程序规约的实例在书写程序规约时，使用Q表示前置断言，R表示后71程序规约的实例例2：求两个非负整数的最大公约数。[ina,b:integer;outy:integer]Q:{a≥0∧b≥0}SR:{y＝MAX(i:1≤i≤min(a,b)∧(amodi＝0)∧(bmodi＝0))}程序规约的实例例2：求两个非负整数的最大公约数。72程序正确性定义衡量一个程序的正确性，主要看程序是否实现了问题所要求的功能。若程序实现了问题所要求的功能，则称它为正确的，否则是不正确的。对程序的正确性理解，可以分为两个层次：从广义来说，一个程序的正确性取决于该程序满足问题实际需求的程度。从狭义而言，如果一个程序满足了它的程序规约就是正确的。程序设计过程：问题程序规约程序程序正确性定义衡量一个程序的正确性，主要看程序是否实现了问题73程序正确性定义程序规约Q{S}R是一个逻辑表达式，其取值为真或假。 其中取值为真的含义是指：给定一段程序S，若程序开始执行之前Q为真，S的执行将终止，且终止时R为真，则称为“程序S，关于前置断言Q和后置断言R是完全正确的”。程序正确性定义程序规约Q{S}R是一个逻辑表达式，其取值为真74程序正确性定义部分正确： 若对于每个使得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是完全正确的。一个程序的完全正确，等价于该程序是部分正确，同时又是终止的。程序正确性定义部分正确：75程序正确性的证明方法分类证明部分正确性的方法

A.Floyd的不变式断言法

B.Manna的子目标断言法

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

A.Floyd的良序集方法

B.Knuth的计数器方法

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

A.Hoare公理化方法的推广

B.Burstall的间发断言法

C.Dijkstra的弱谓词变换方法以及强验证方法程序正确性的证明方法分类证明部分正确性的方法76第5章程序正确性证明5.1程序正确性验证概述5.2不变式断言法5.3子目标断言法5.4界函数法－－计数器法第5章程序正确性证明5.1程序正确性验证概述77循环不变式断言把反映循环变量的变化规律，且在每次循环体的执行前后均为真的逻辑表达式称为该循环的不变式断言。

例带余整数除法问题：设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循环不变式断言把反映循环变量的变化规律，且在每次循环体的执行785.2不变式断言法证明步骤：1、建立断言 建立程序的输入、输出断言，如果程序中有循环出现的话，在循环中选取一个断点，在断点处建立一个循环不变式断言。2、建立检验条件 将程序分解为不同的通路，为每一个通路建立一个检验条件，该检验条件为如下形式：

I∧R=>O

其中I为输入断言，R为进入通路的条件，O为输出断言。3、证明检验条件 运用数学工具证明步骤2得到的所有检验条件，如果每一条通路检验条件都为真，则该程序为部分正确的。5.2不变式断言法证明步骤：79不变式断言法实例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不变式断言法实例1例：设x,y为正整数，求x,y的最大公约数80不变式断言法实例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······不变式断言法实例1(建立断言)输入断言：通路划分：ST81不变式断言法实例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)不变式断言法实例1(建立检验条件)检验条件：I∧R=82不变式断言法实例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)不变式断言法实例1(建立检验条件)通路3：83不变式断言法实例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)不变式断言法实例1(证明检验条件)通路1：84不变式断言法实例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····不变式断言法实例2对任一给定的自然数x，计算z＝[85不变式断言法实例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不变式断言法实例2检验条件：I∧R=>O86不变式断言法实例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不变式断言法实例2检验条件287作业课本P174习题1、习题2。要求用不变式断言法证明。作业课本P174习题1、习题2。要求用不变式断言法证明。88第5章程序正确性证明5.1程序正确性验证概述5.2不变式断言法5.3子目标断言法5.4界函数法－－计数器法第5章程序正确性证明5.1程序正确性验证概述895.3子目标断言法子目标断言法与不变式断言法的主要区别是：两种方法对循环所建立的断言不同。不变式断言描述了程序变量y的中间值与初始值之间关系；子目标断言法描述的是y的中间值与循环终止时的最终值yend之间的关系。两种方法进行归纳的方向不同。不变式断言沿着程序正常执行的方向进行归纳；子目标断言法则沿着相反方向进行归纳。5.3子目标断言法子目标断言法与不变式断言法的主要区别是：90不变式断言法输入断言： 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······不变式断言法输入断言：例：设x,y为非负整数，求x,y的最大91子目标断言法(建立断言)输入断言

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······子目标断言法(建立断言)输入断言STARTRe92子目标断言法(建立检验条件)通路1： 控制转出循环时，子目标断言成立。通路2、通路3： 如果在通过循环之后，子目标断言在断点处成立，那么，在通过循环之前，断言也成立。通路4： 如果输入断言为真，且控制第一次通过断点B时子目标断言为真，则输出断言为真。子目标断言法(建立检验条件)通路1：93子目标断言法(建立检验条件)通路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)子目标断言法(建立检验条件)通路1：b->c94子目标断言法(证明检验条件)检验条件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)]

子目标断言法(证明检验条件)检验条件1：95程序部分正确但不终止实例例：求两个非负整数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时，程序循环将不终止！

程序部分正确但不终止实例例：求两个非负整数x、y的最大公约数96第5章程序正确性证明5.1程序正确性验证概述5.2不变式断言法5.3子目标断言法5.4界函数法－－计数器法第5章程序正确性证明5.1程序正确性验证概述975.4计数器方法证明程序终止性证明思路 通过估计循环执行的最大次数证明程序终止性的方法。证明步骤:1.为程序的每一个循环附加一个新的变量作为该循环的计数器，初始值置为0，每循环一次该计数器加1。2.为每个循环设置一个中间断言，它表示相应的计数器不会超过固定的界限。3.证明（2）中的中间断言是不变式断言。5.4计数器方法证明程序终止性证明思路98计数器方法证明程序终止性实例计算非负整数的最大公约数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·计数器方法证明程序终止性实例计算非负整数的最大公约数var99计数器方法证明程序终止性实例1.引进计数器I,并建立如下断言

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

varx,y,z,s:integer;