程序正确性证明

程序正确性证明主要内容•程序正确性简介•程序测试•程序正确性证明内容线索•程序正确性简介•程序测试•程序正确性证明程序的正确性•所谓一段程序是正确的，是指这段程序能准确无误地完成编写者所期望赋予它的功能。–或者说，对任何一组允许的输入信息，程序执行后能得到一组和这组输入信息相对应的正确的输出信息。–通俗地说，“做了它该做的事，没有做它不该做的事”•程序正确性的严格定义分为三种类型–部分正确性–终止性–完全正确性如何保证程序的正确性•要求–1、从编程时就应该尽量地避免和减少错误的发生–2、当程序编好后要尽量找出错误，纠正错误•避免错误的方法–1、程序的结构要简单–2、采用标准的软件设计工具、标准的算法手册以及有效的程序设计方法•发现错误的方法–1、利用测试工具–2、利用程序的验证系统内容线索程序正确性简介•程序测试•程序正确性证明程序测试•测试是程序的执行过程，目的在于发现错误。–一个好的测试用例在于能发现至今未发现的错误；–一个成功的测试是发现了至今未发现的错误的测试。•测试的原则–1.应当“尽早地和不断地进行软件测试”。–2.测试用例应由测试输入数据和对应的预期输出结果组成。–3.程序员应避免检查自己的程序。–4.在设计测试用例时，应当包括合理的输入条件和不合理的输入条件。–5.充分注意测试中的群集现象。即测试后程序中残存的错误数目与该程序中已发现的错误数目成正比。–6.严格执行测试计划，排除测试的随意性。–7.应当对每一个测试结果做全面检查。–8.妥善保存测试计划，测试用例，出错统计和最终分析报告，为维护提供方便。内容线索程序正确性简介程序测试•程序正确性证明–简介–Floyd不变式断言法–Hoare规则公理方法–Dijkstra最弱前置条件方法正确性证明•测试只能发现程序错误，但不能证明程序无错。即所谓“挂一漏万”。–原因：测试并没有也不可能包含所有数据，只是选择了一些具有代表性的数据，所以它具有局限性。•正确性证明是通过数学技术来确定软件是否正确，也就是说，是否符合其规格说明。正确性证明的发展50年代1967年1969年1973年1975年1976年1979年1980年第一个基于公理和推导规则的自动验证系统出现。Dijkstra提出最弱前置谓词和谓词转换器的概念。出现了用公理化思想定义的程序设计语言——Euclid。同年，Perlis批评程序正确性证明不切实际。Gries综合了以谓词演算为基础的证明系统，称为程序设计科学。首次把程序设计从经验技术升华为科学。Turing等Floyd用断言方法证明框图程序的正确性Hoare定义一个逻辑系统，含有程序公理和推导规则。目的侧重于程序的部分正确性。此系统是一阶谓词逻辑的扩充。这就是著名的Hoare逻辑。Hoare是第一个从正确性证明角度定义程序语言的。Hoare和Wirth把Pascal的大部分公理化。Manna把部分正确性证明和终止性证明归于一体。正确性证明的方法•为了证明一个程序的完全正确性，通常采用的方法是分别证明该程序的部分正确性和终止性。•主要方法有：–关于部分正确性证明的方法•Floyd的不变式断言法(*)•Manna的子目标断言法•Hoare的公理化方法(*)–关于终止性证明的方法•Floyd的良序集方法(*)•Manna等人的不动点方法•Knuth的计数器方法–关于完全正确性证明的方法•Hoare的公理化方法的推广（Manna，Pnueli）•Burstall的间发断言方法•Dijkstra最弱前置谓词变换方法以及强验证方法(*)预备知识…•前置(输入)断言:输入应满足的条件•后置(输出)断言:输入出应满足的条件•程序规范：程序的前置断言和程序的后置断言组成•程序的状态：程序执行到某一时刻，程序中所有变量的一组取值•初始状态：所有变量的取值使程序的前置断言为真的状态•终止状态：所有变量的取值使程序的后置断言为真的状态•程序的执行可以看作是程序状态的变迁逻辑谓词前提条件，初始状态前置断言程序，语句结论，终止状态满足的条件后置断言逻辑谓词…预备知识•1、完全正确性断言：程序S的执行开始于满足P的状态，则该执行必定能在有限的时间内终止，且终止的状态满足Q，则称完全正确性断言，记为{P}S{Q}•2、部分正确性断言：程序S的执行开始于满足P的状态，若此执行能在有限的时间内终止，则终止时的状态满足Q，则称部分正确性断言，记为[P]S[Q]程序正确性概念•定义1.如果对于每一个使得P(ā)为真的输入ā，程序S计算都终止，称程序S对P是终止的。•定义2：对于满足P(ā)为真，且能够使程序S计算终止的每个ā，如果Q(ā,P(ā))为真，则称程序S对于P和Q是部分正确的。记为[P]S[Q]。•定义3：对于满足P(ā)为真的每个ā，如果程序S能够计算终止，且Q(ā,P(ā))为真，则称程序S对于P和Q是完全正确的。记为{P}S{Q}不变式断言法•R.W.Floyd，1967年提出•证明一个程序的部分正确性–步骤–（1）建立断言•输入断言((x))：前提条件，初始状态•输出断言((x,z))：最终结论，终止状态满足的条件•循环不变式：在每次循环的前后均为真的谓词–（2）建立检验条件•检验条件：程序运行通过该通路时应满足的条件–（3）证明检验条件•适合对象：程序流程图i(x,y)Ri(x,y)i(x,ri(x,y))输入断言输出断言y：一组中间变量x：输入变量xy：蕴含符，即ri(x,y)：通过该通路后y的值通过此路径的条件实例•设x1,x2是正整数，求它们的最大公约数z=gcd(x1,x2)。我们知道，对于任意正整数y1,y2，有下列关系：(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开始(x1,x2)(y1,y2)y1=y2y1y2y1-y2y1y2-y1y2A…(x)B…P(x,y)y1zG结束C…(x,z)DETFFT证明…•(1)建立断言(x)：x10x20(x,z)：z=gcd(x1,x2)P(x,y)：x10x20y10y20gcd(y1,y2)=gcd(x1,x2)•(2)建立检验条件通路1：A--B;通路2：B--D--B通路3：B--E--B;通路4：B--G--C为每一条通过，建立检验条件通路1：A--B无条件，R1(x,y)恒真，结果y取值为x。检验条件为：(x)P(x,y)即[x10x20]x10x20y10y20gcd(x1,x2)=gcd(x1,x2)开始(x1,x2)(y1,y2)y1=y2y1y2y1-y2y1y2-y1y2A…(x)B…P(x,y)y1zG结束C…(x,z)DETFFT…证明…通路2：B--D--BR2(x,y)=[y1y2y1y2]r2(x,y)=(y1-y2,y2)P(x,y)输入输出均为P(x,y)检验条件为：[P(x,y)y1y2y1y2]P(x,(y1-y2,y2))将断言P(x,y)代入，即得[x10x20y10y20gcd(y1,y2)=gcd(x1,x2)y1y2y1y2][x10x20y1-y20y20gcd(y1-y2,y2)=gcd(x1,x2)]通路3：B--E--B类似地，得到[P(x,y)y1y2y1y2]P(x,y1,y2-y1)通路4：B--G--C类似地，得到[P(x,y)y1=y2](x,z)开始(x1,x2)(y1,y2)y1=y2y1y2y1-y2y1y2-y1y2A…(x)B…P(x,y)y1zG结束C…(x,z)DETFFT…证明•(3)证明检验条件通路1：[x10x20]x10x20gcd(x1,x2)=gcd(x1,x2)显然通路2：[x10x20y10y20gcd(y1,y2)=gcd(x1,x2)y1y2y1y2][x10x20y1-y20y20gcd(y1-y2,y2)=gcd(x1,x2)]检验条件前项成立时，y1y2为真，而y1-y20为真且gcd(y1-y2,y2)=gcd(y1,y2)=gcd(x1,x2)检验条件为真通路3：[P(x,y)y1y2y1y2]P(x,y1-y2,y2-y1)y1y2为真,y1-y20为真,gcd(y1,y2-y1)=gcd(y1,y2)=gcd(x1,x2)检验条件为真通路4：[P(x,y)y1=y2](x,z)y1=y2,gcd(y1,y2)=y1=y2,检验条件为真同步练习开始(0,0,1)(y1,y2,y3)y2x(y1+1,y3+2)(y1,y3)A…(x)B…P(x,y)y1z结束C…(x,z)DTFy2+y3y2B’内容线索程序正确性简介程序测试•程序正确性证明简介Floyd不变式断言法–Hoare规则公理方法–Dijkstra最弱前置条件方法程序正确性验证–Hoare公理学方法•1990年IEEE计算机先驱奖•1980年图灵奖•英国牛津大学计算机科学家查尔斯.霍尔(CharlesAntonyRichardHoare)•发明Quicksort算法、CASE语句•1963年实现了Algol语言•1969年1月，在Comm.OfACM上发表“AnAxiomaticbasisforComputerProgramming”,提出公理语义学•操作系统的Monitor•ACM在1983年评出在近25年在CACM上发表的25篇里程碑式的论文25篇，2人2篇，Hoare是其一Hoare公理学方法•在Floyd的归纳法断言基础上，C.A.R.Hoare于1969年发表了“计算机程序设计的公理基础”一文，提出了另一种程序验证的方法，他的成功在于使用了简洁的符号和提出了定义程序语义的公理系统。Hoare公理系统和Hoare逻辑是十多年来引人注目的重要工作。•Hoare系统是一个关于形如[P]S[Q]的断言的逻辑系统。[P]S[Q]是为了区别于完全正确的{P}S{Q}断言的部分正确性断言的表示方法。这是方法是针对WHILE型程序提出的。Hoare公理学方法-部分正确性证明1.WHILE型程序WHILE型程序是由一个有限的语句序列组成，每个语句之间的分号隔开，即：B0；B1；...Bn其中，B0是程序中唯一的开始语句：STARTyf(x)Bi(1=i=n)是下列语句之一：程序正确性验证–Hoare公理学方法1)赋值语句：yg(x,y)2)条件语句：ifRthenF1elseF2或ifRthenF13)复合：BeginF1，F2，...，FnEnd4)循环语句：whileRdoF15)停机语句：Zh(x,y)HALT其中，语句R是逻辑表达式，F1，F2，...，Fn是上列语句中的任何一种。程序正确性验证–Hoare公理学方法•例如：计算Z=sqrt(x)的程序：START(y1,y2,y3)(0,1,1);While(y2=x)do(y1,y2,y3)(y1+1,y2+y3+2,y3+2);Zy1;HALT程序正确性验证–Hoare公理学方法•2.不变式演绎系统—Hoare系统1）基本概念（1）不变式语句:[P]F[Q]其中，P,Q是逻辑表达式，F是一个程序段。它的含义是:“如果执行F以前P成立，且执行终止，则执行F后Q成立”,这时不变式语句为真，有时也称为归纳表达式。程序正确性验证–Hoare公理学方法1）基本概念（2）推理规则A1,A2,…,AnB其中，B是一个不变式语句，Ai(i=1,2,…,n)是一个逻辑表达式或者是其它的不变式语句。它的含义：“为了推导后项为真，只需证明前项A1,A2,…,An为真”.2.不变式演绎系统—Hoare系统程序正确性