程序正确性证明1学习教案

1、会计学1程序正确性证明程序正确性证明(zhngmng)1第一页，共63页。第1页/共62页第二页，共63页。n终止性终止性n完全正确性完全正确性第2页/共62页第三页，共63页。n1、利用测试工具、利用测试工具n2、利用程序的验证系统、利用程序的验证系统第3页/共62页第四页，共63页。第4页/共62页第五页，共63页。第5页/共62页第六页，共63页。第6页/共62页第七页，共63页。第7页/共62页第八页，共63页。第8页/共62页第九页，共63页。第9页/共62页第十页，共63页。第10页/共62页第十一页，共63页。第11页/共62页第十二页，共63页。第12页/共62页第十三页，共6

2、3页。第13页/共62页第十四页，共63页。第14页/共62页第十五页，共63页。50年代1967年1969年1973年1975年1976年1979年1980年第一个基于公理和推导规则的自动验证系统出现。Dijkstra提出最弱前置谓词和谓词转换器的概念。出现了用公理化思想定义的程序设计语言Euclid。同年，Perlis批评程序正确性证明不切实际。Gries综合了以谓词演算为基础的证明系统，称为程序设计科学。首次把程序设计从经验技术升华为科学。Turing等Floyd用断言方法证明框图程序的正确性Hoare定义一个逻辑系统，含有程序公理和推导规则。目的侧重于程序的部分正确性。此系统是一阶谓词

3、逻辑的扩充。这就是著名的Hoare逻辑。Hoare是第一个从正确性证明角度定义程序语言的。Hoare和Wirth把Pascal的大部分公理化。Manna把部分正确性证明和终止性证明归于一体。第15页/共62页第十六页，共63页。第16页/共62页第十七页，共63页。程序正确性理论程序正确性理论(lln) 程序功能程序功能(gngnng)的精确描述的精确描述 1、程序规约：对程序所实现、程序规约：对程序所实现(shxin)功能的精确描述，功能的精确描述， 由程序的前置断言和后置断言两部分组成。由程序的前置断言和后置断言两部分组成。2、前置断言：程序执行前的输入应满足的条件，、前置断言：程序执行前

4、的输入应满足的条件， 又称为输入断言。又称为输入断言。3、后置断言：程序执行后的输出应满足的条件，、后置断言：程序执行后的输出应满足的条件， 又称为输出断言。又称为输出断言。 程序设计过程：问题程序设计过程：问题 程序规约程序规约 程序程序第17页/共62页第十八页，共63页。逻辑谓词逻辑谓词前提条件，初始状态前提条件，初始状态 前置断言前置断言 程序，语句程序，语句 结论，终止状态满足的条件结论，终止状态满足的条件 后置断言后置断言 逻辑谓词逻辑谓词第18页/共62页第十九页，共63页。程序正确性定义程序正确性定义(dngy)第19页/共62页第二十页，共63页。程序正确性定义程序正确性定义

5、(dngy)第20页/共62页第二十一页，共63页。第21页/共62页第二十二页，共63页。为每一个通路建立一个检验条件，该检验条件为为每一个通路建立一个检验条件，该检验条件为如下形式：如下形式：n I R = O,其中其中I为输入断言，为输入断言，R为进入通路的为进入通路的条件，条件，O为输出断言为输出断言第22页/共62页第二十三页，共63页。 i(x,y) Ri(x,y) i(x,r i(x,y)输入输入(shr)断言断言输出输出(shch)断言断言y： 一组中间变量一组中间变量x：输入变量：输入变量xy：蕴含符，即：蕴含符，即 ri(x,y)：通过该通路后通过该通路后y的值的值通过此路

6、径的条件通过此路径的条件第23页/共62页第二十四页，共63页。第24页/共62页第二十五页，共63页。(1) 若若y1y2， gcd(y1,y2)= gcd(y1- y2,y2)(2) 若若y2y1， gcd(y1,y2)= gcd(y1,y2 - y1)(1) 若若y1=y2， gcd(y1,y2)= y1=y2开始开始(kish)(x1,x2) (y1,y2)y1=y2y1y2y1-y2 y1y2-y1 y2 A (x) B P(x,y)y1 zG结束结束C (x,z)DETF F T第25页/共62页第二十六页，共63页。n为每一条通过，建立检验为每一条通过，建立检验(jinyn)条件

7、条件开始开始(x1,x2) (y1,y2)y1=y2y1y2y1-y2 y1y2-y1 y2 A (x) B P(x,y)y1 zG结束结束C (x,z)DETF F T第26页/共62页第二十七页，共63页。开始开始(x1,x2) (y1,y2)y1=y2y1y2y1-y2 y1y2-y1 y2 A (x) B P(x,y)y1 zG结束结束C (x,z)DETF F T证明证明(zhngmng)第27页/共62页第二十八页，共63页。开始开始(x1,x2) (y1,y2)y1=y2y1y2y1-y2 y1y2-y1 y2 A (x) B P(x,y)y1 zG结束结束C (x,z)DETF

8、 F T第28页/共62页第二十九页，共63页。开始开始(x1,x2) (y1,y2)y1=y2y1y2y1-y2 y1y2-y1 y2 A (x) B P(x,y)y1 zG结束结束C (x,z)DETF F T第29页/共62页第三十页，共63页。第30页/共62页第三十一页，共63页。开始(0,1,1)-(y1,y2,y3)y2+y3-y2y2x(y1+1,y3+2)-(y1,y3)y1-z结束A I(x)B P(x,y1,y2,y3)DC O(x,z)TFxB第31页/共62页第三十二页，共63页。第32页/共62页第三十三页，共63页。第33页/共62页第三十四页，共63页。开始(k

9、ish)(0,0,1) (y1,y2,y3)y2x(y1+1,y3+2) (y1,y3) A (x) B P(x,y)y1 z结束(jish)C (x,z)DTF y2+y3 y2B第34页/共62页第三十五页，共63页。第35页/共62页第三十六页，共63页。子目标断言子目标断言(dunyn)法法子目标断言法与不变式断言法的主要区别是：子目标断言法与不变式断言法的主要区别是：两种方法对循环两种方法对循环(xnhun)所建立的断言不同。不变式断言描述了程序所建立的断言不同。不变式断言描述了程序变量变量y的中间值与初始值之间关系，而子目标断言法描述的是的中间值与初始值之间关系，而子目标断言法描述

10、的是y的中的中间值与循环间值与循环(xnhun)终止时的最终值终止时的最终值yend之间的关系。之间的关系。两种方法进行归纳的方向不同。不变式断言沿着程序正常执行的方向两种方法进行归纳的方向不同。不变式断言沿着程序正常执行的方向进行归纳，而子目标断言法则沿着相反方向进行归纳。进行归纳，而子目标断言法则沿着相反方向进行归纳。第36页/共62页第三十七页，共63页。STARTRead(x,y)x0y=xy:=y-xx yz:=ySTOPTFTFI(x,y)aP(x,y)bcO(x,y,z)deg例：设例：设x,y为正整数，求为正整数，求x,y的最的最大公约数大公约数z的程序的程序(chngx)，即

11、即z=gcd(x,y)。第37页/共62页第三十八页，共63页。STARTRead(x,y)x0y=xy:=y-xx yz:=ySTOPTFTFI(x,y)aP(x,y)bcO(x,y,z)deg当控制以当控制以x,y的容许值通过的容许值通过L时，时，x,y的当前的当前(dngqin)值的最大公值的最大公约数等于约数等于y 的最终值。的最终值。第38页/共62页第三十九页，共63页。 yx =x=0 y=0 yend = gcd(x,y)第39页/共62页第四十页，共63页。第40页/共62页第四十一页，共63页。第41页/共62页第四十二页，共63页。第42页/共62页第四十三页，共63页。

12、第43页/共62页第四十四页，共63页。第44页/共62页第四十五页，共63页。第45页/共62页第四十六页，共63页。 (2)条件规则条件规则 S1Q和和 S2Q为表示方便，我们可用证明规则的一般形式为表示方便，我们可用证明规则的一般形式(xngsh)显然，上述条件语句的二种形式显然，上述条件语句的二种形式(xngsh)分别可表示为分别可表示为 BP BP,QSthenBifPQBPQSBP,2121QSelseSthenBifPQSBPQSBP第46页/共62页第四十七页，共63页。（3）while规则规则(guz) 1) while B do S PI,I RFI,I R=Q P whi

13、le R do FQ PI表示表示(biosh)当控制进入循环时，不变式当控制进入循环时，不变式I为真；为真；条件条件IRFI表示表示(biosh)I是不变式，即如是不变式，即如果执行果执行F前前I为真为真,且且F执行终止，则执行终止，则F执行后执行后I仍仍为真。为真。 条件条件I R=Q 表示表示(biosh)如果控如果控制退出循环，制退出循环，Q将是真。将是真。第47页/共62页第四十八页，共63页。第48页/共62页第四十九页，共63页。 P:trueP A0B:=AB0 B 0P A 0B:= -AB 0则，则，trueif A0 then B:=A else B=-AB 0例：例：

14、计算计算X=MAX(A,B)的程序的程序(chngx)为为if A B then X:=A else X:=B. 试验证其正确性。试验证其正确性。 证明证明(zhngmng)：P:trueP A BX:=AX=A X BP AA 而而 X=A X B X=MAX(A,B) X=B XA X=MAX(A,B) 故故P:true if A B then X:=A else X:=B. X=MAX(A,B) 例：例： 第49页/共62页第五十页，共63页。明明(zhngmng)这些逻辑表达式成立。这样就证这些逻辑表达式成立。这样就证明明(zhngmng)了程序的部分正确性。了程序的部分正确性。第50页/共62页第五十一页，共63页。nHALT第51页/共62页第五十二页，共63页。n(x,y1+1,y2+y3+2,y3+2)P(x,y)第52页/共62页第五十三页，共63页。第53页/共62页第五十四页，共63页。n第54页/共62页第五十五页，共63页。第