程序正确性证明1PPT课件

3 - 1内容线索内容线索程序正确性简介程序正确性简介程序测试程序测试程序正确性证明程序正确性证明第1页/共62页3 - 2程序的正确性程序的正确性所谓一段程序是正确的，是指这段程序能准确无误所谓一段程序是正确的，是指这段程序能准确无误地完成编写者所期望赋予它的功能。地完成编写者所期望赋予它的功能。或者说，对任何一组允许的输入信息，程序执行后或者说，对任何一组允许的输入信息，程序执行后能得到一组和这组输入信息相对应的正确的输出信能得到一组和这组输入信息相对应的正确的输出信息。息。通俗地说，通俗地说，“做了它该做的事，没有做它不该做的做了它该做的事，没有做它不该做的事事”程序正确性的严格定义分为三种类型程序正确性的严格定义分为三种类型部分正确性部分正确性终止性终止性完全正确性完全正确性第2页/共62页3 - 3如何保证程序的正确性如何保证程序的正确性要求要求1、从编程时就应该尽量地避免和减少错误的发生、从编程时就应该尽量地避免和减少错误的发生2、当程序编好后要尽量找出错误，纠正错误、当程序编好后要尽量找出错误，纠正错误避免错误的方法避免错误的方法1、程序的结构要简单、程序的结构要简单2、采用标准的软件设计工具、标准的算法手册以及、采用标准的软件设计工具、标准的算法手册以及有效的程序设计方法有效的程序设计方法发现错误的方法发现错误的方法1、利用测试工具、利用测试工具2、利用程序的验证系统、利用程序的验证系统第3页/共62页3 - 4内容线索内容线索程序正确性简介程序正确性简介程序测试程序测试程序正确性证明程序正确性证明第4页/共62页3 - 5程序测试程序测试测试是程序的执行过程，目的在于发现错误。测试是程序的执行过程，目的在于发现错误。一个好的测试用例在于能发现至今未发现的错误；一个好的测试用例在于能发现至今未发现的错误； 一个成功的测试是发现了至今未发现的错误的测试。一个成功的测试是发现了至今未发现的错误的测试。测试的原则测试的原则1. 应当应当 “尽早地和不断地进行软件测试尽早地和不断地进行软件测试” 。2. 测试用例应由测试输入数据和对应的预期输出结果组成。测试用例应由测试输入数据和对应的预期输出结果组成。3. 程序员应避免检查自己的程序。程序员应避免检查自己的程序。4. 在设计测试用例时，应当包括合理的输入条件和不合理的在设计测试用例时，应当包括合理的输入条件和不合理的输入条件。输入条件。5. 充分注意测试中的群集现象。即测试后程序中残存的错误充分注意测试中的群集现象。即测试后程序中残存的错误数目与该程序中已发现的错误数目成正比。数目与该程序中已发现的错误数目成正比。6. 严格执行测试计划，排除测试的随意性。严格执行测试计划，排除测试的随意性。7. 应当对每一个测试结果做全面检查。应当对每一个测试结果做全面检查。8. 妥善保存测试计划，测试用例，出错统计和最终分析报妥善保存测试计划，测试用例，出错统计和最终分析报告，为维护提供方便。告，为维护提供方便。第5页/共62页3 - 6程序测试的过程程序测试的过程第6页/共62页3 - 7程序测试的过程程序测试的过程第7页/共62页3 - 8程序测试的方法程序测试的方法两种常用的测试方法两种常用的测试方法 黑盒测试黑盒测试这种方法是把测试对象看做一个黑盒子，测试人员完全不这种方法是把测试对象看做一个黑盒子，测试人员完全不考虑程序内部的逻辑结构和内部特性，只依据程序的需求考虑程序内部的逻辑结构和内部特性，只依据程序的需求规格说明书，检查程序的功能是否符合它的功能说明。规格说明书，检查程序的功能是否符合它的功能说明。黑盒测试又叫做功能测试或数据驱动测试。黑盒测试又叫做功能测试或数据驱动测试。 白盒测试白盒测试此方法把测试对象看做一个透明的盒子，它允许测试人员此方法把测试对象看做一个透明的盒子，它允许测试人员利用程序内部的逻辑结构及有关信息，设计或选择测试用利用程序内部的逻辑结构及有关信息，设计或选择测试用例，对程序所有逻辑路径进行测试。例，对程序所有逻辑路径进行测试。通过在不同点检查程序的状态，确定实际的状态是否与预通过在不同点检查程序的状态，确定实际的状态是否与预期的状态一致。因此白盒测试又称为结构测试或逻辑驱动期的状态一致。因此白盒测试又称为结构测试或逻辑驱动测试。测试。第8页/共62页3 - 9黑盒测试黑盒测试黑盒测试方法是在程序接口上进行测试，主要是为了发现以黑盒测试方法是在程序接口上进行测试，主要是为了发现以下错误下错误: 是否有不正确或遗漏了的功能是否有不正确或遗漏了的功能? 在接口上，输入能否正确地接受在接口上，输入能否正确地接受? 能否输出正确的结果能否输出正确的结果? 是否有数据结构错误或外部信息是否有数据结构错误或外部信息(例如数据文件例如数据文件)访问错误访问错误? 性能上是否能够满足要求性能上是否能够满足要求? 是否有初始化或终止性错误是否有初始化或终止性错误?用黑盒测试发现程序中的错误，必须在所有可能的输入条件用黑盒测试发现程序中的错误，必须在所有可能的输入条件和输出条件中确定测试数据，来检查程序是否都能产生正确和输出条件中确定测试数据，来检查程序是否都能产生正确的输出。的输出。但这是不可能的。但这是不可能的。第9页/共62页3 - 10白盒测试白盒测试软件人员使用白盒测试方法，主要想对程序模块进软件人员使用白盒测试方法，主要想对程序模块进行如下的检查：行如下的检查： 对程序模块的所有独立的执行路径至少测试一次；对程序模块的所有独立的执行路径至少测试一次； 对所有的逻辑判定，取对所有的逻辑判定，取“真真”与取与取“假假”的两种情的两种情况都至少测试一次；况都至少测试一次； 在循环的边界和运行界限内执行循环体；在循环的边界和运行界限内执行循环体； 测试内部数据结构的有效性等。测试内部数据结构的有效性等。第10页/共62页3 - 11白盒测试白盒测试对一个具有多重选择和循环嵌套的程序，不同的路对一个具有多重选择和循环嵌套的程序，不同的路径数目可能是天文数字。给出一个小程序的流程径数目可能是天文数字。给出一个小程序的流程图，它包括了一个执行图，它包括了一个执行20次的循环。次的循环。包含的不同执行路径数达包含的不同执行路径数达520条，对每一条路径进行条，对每一条路径进行测试需要测试需要1毫秒，假定一年工作毫秒，假定一年工作365 24小时，要小时，要想把所有路径测试完，需想把所有路径测试完，需3170年。年。第11页/共62页3 - 12白盒测试白盒测试语句覆盖语句覆盖判定覆盖判定覆盖 条件覆盖条件覆盖 判定条件覆盖判定条件覆盖 条件组合覆盖条件组合覆盖 路径覆盖路径覆盖第12页/共62页3 - 13内容线索内容线索程序正确性简介程序正确性简介程序测试程序测试程序正确性证明程序正确性证明简介简介Floyd不变式断言法不变式断言法子目标断言法子目标断言法Hoare规则公理方法规则公理方法第13页/共62页3 - 14正确性证明正确性证明测试只能发现程序错误，但不能证明程序无错。测试只能发现程序错误，但不能证明程序无错。原因：测试并没有也不可能包含所有数据，只是选原因：测试并没有也不可能包含所有数据，只是选择了一些具有代表性的数据，所以它具有局限性。择了一些具有代表性的数据，所以它具有局限性。正确性证明是通过数学技术来确定软件是否正确，正确性证明是通过数学技术来确定软件是否正确，也就是说，是否符合其规格说明。也就是说，是否符合其规格说明。第14页/共62页3 - 15正确性证明的发展正确性证明的发展50年代1967年1969年1973年1975年1976年1979年1980年第一个基于公理和推导规则的自动验证系统出现。Dijkstra提出最弱前置谓词和谓词转换器的概念。出现了用公理化思想定义的程序设计语言Euclid。同年，Perlis批评程序正确性证明不切实际。Gries综合了以谓词演算为基础的证明系统，称为程序设计科学。首次把程序设计从经验技术升华为科学。Turing等Floyd用断言方法证明框图程序的正确性Hoare定义一个逻辑系统，含有程序公理和推导规则。目的侧重于程序的部分正确性。此系统是一阶谓词逻辑的扩充。这就是著名的Hoare逻辑。Hoare是第一个从正确性证明角度定义程序语言的。Hoare和Wirth把Pascal的大部分公理化。Manna把部分正确性证明和终止性证明归于一体。第15页/共62页3 - 16正确性证明的方法正确性证明的方法为了证明一个程序的完全正确性，通常采用的方法是分别证为了证明一个程序的完全正确性，通常采用的方法是分别证明该程序的部分正确性和终止性。明该程序的部分正确性和终止性。主要方法有：主要方法有：关于部分正确性证明的方法关于部分正确性证明的方法Floyd的不变式断言法的不变式断言法(*)Manna的子目标断言法的子目标断言法Hoare的公理化方法的公理化方法(*)关于终止性证明的方法关于终止性证明的方法Floyd的良序集方法的良序集方法(*)Manna等人的不动点方法等人的不动点方法Knuth的计数器方法的计数器方法关于完全正确性证明的方法关于完全正确性证明的方法Hoare的公理化方法的推广（的公理化方法的推广（ Manna ，Pnueli）Burstall的间发断言方法的间发断言方法Dijkstra最弱前置谓词变换方法以及强验证方法最弱前置谓词变换方法以及强验证方法(*)第16页/共62页3 - 17程序正确性理论程序正确性理论 程序功能的精确描述程序功能的精确描述 1、程序规约：对程序所实现功能的精确描述，、程序规约：对程序所实现功能的精确描述， 由程序的前置断言和后置断言两部分组成。由程序的前置断言和后置断言两部分组成。2、前置断言：程序执行前的输入应满足的条件，、前置断言：程序执行前的输入应满足的条件， 又称为又称为输入输入断言。断言。3、后置断言：程序执行后的输出应满足的条件，、后置断言：程序执行后的输出应满足的条件， 又称为又称为输出输出断言。断言。 程序设计过程：问题程序设计过程：问题 程序规约程序规约 程序程序第17页/共62页3 - 18预备知识预备知识程序的状态：程序执行到某一时刻，程序中所有变量的一组程序的状态：程序执行到某一时刻，程序中所有变量的一组取值取值初始状态：所有变量的取值使程序的前置断言为真的状态初始状态：所有变量的取值使程序的前置断言为真的状态终止状态：所有变量的取值使程序的后置断言为真的状态终止状态：所有变量的取值使程序的后置断言为真的状态程序的执行可以看作是程序状态的变迁程序的执行可以看作是程序状态的变迁逻辑谓词逻辑谓词前提条件，初始状态前提条件，初始状态 前置断言前置断言 程序，语句程序，语句 结论，终止状态满足的条件结论，终止状态满足的条件 后置断言后置断言 逻辑谓词逻辑谓词第18页/共62页3 - 19程序规约程序规约QSR是一个逻辑表达式，其取值为真或是一个逻辑表达式，其取值为真或假，其中取值为真的含义是指：给定一段程序假，其中取值为真的含义是指：给定一段程序S，若，若程序开始执行之前程序开始执行之前Q为真，为真，S的执行将终止，且终止的执行将终止，且终止时时R为真，则称为为真，则称为 “程序程序S，关于前置断言，关于前置断言Q和后置和后置断言断言R是是完全正确完全正确的的”。程序正确性定义程序正确性定义第19页/共62页3 - 20部分正确部分正确：若对于每个使得：若对于每个使得Q(i)为真，并且程序为真，并且程序S计算终止的输入计算终止的输入信息信息i，R(i,S(i)都为真，则称程序都为真，则称程序S关于关于Q和和R是部分正确的。是部分正确的。程序终止程序终止：若对于每个使得：若对于每个使得Q(i)为真的输入为真的输入i，程序，程序S的计算都终的计算都终止，则称程序止，则称程序S关于关于Q是终止的。是终止的。完全正确完全正确：若对于每个使得：若对于每个使得Q(i)为真，并且程序为真，并且程序S的计算都将终止的计算都将终止的输入信息的输入信息i，R(i,S(i)都为真，则称程序都为真，则称程序S关于关于Q和和R是完全正确是完全正确的。的。一个程序的一个程序的完全正确完全正确，等价于该程序是，等价于该程序是部分正确部分正确，同时又是，同时又是终止终止的。的。程序正确性定义程序正确性定义第20页/共62页3 - 21内容线索内容线索程序正确性简介程序正确性简介程序测试程序测试程序正确性证明程序正确性证明简介简介Floyd不变式断言法不变式断言法Hoare规则公理方法规则公理方法Dijkstra最弱前置条件方法最弱前置条件方法Dijkstra最弱前置条件方法最弱前置条件方法第21页/共62页3 - 22，1967年提出年提出证明一个程序的部分正确性证明一个程序的部分正确性步骤步骤（1）建立断言）建立断言前置断言前置断言( (x)：前提条件，初始状态：前提条件，初始状态后置断言后置断言( (x,z)：最终结论，终止状态满足的条件：最终结论，终止状态满足的条件循环不变式：在循环中选取一个断点，在断点处建立一个循环不变式：在循环中选取一个断点，在断点处建立一个适当的断言，使循环每次执行到断点时，断言都为真适当的断言，使循环每次执行到断点时，断言都为真（2）建立检验条件，将程序分解为不同的通路，为每一个）建立检验条件，将程序分解为不同的通路，为每一个通路建立一个检验条件，该检验条件为如下形式：通路建立一个检验条件，该检验条件为如下形式： I R = O,其中其中I为输入断言，为输入断言，R为进入通路的条件，为进入通路的条件，O为输出断言为输出断言不变式断言法不变式断言法第22页/共62页3 - 23（2）建立检验条件）建立检验条件检验条件：程序运行通过该通路时应满足的条件检验条件：程序运行通过该通路时应满足的条件 i(x,y) Ri(x,y) i(x,r i(x,y)输入断言输入断言输出断言输出断言y： 一组中间变量一组中间变量x：输入变量：输入变量xy：蕴含符，即：蕴含符，即 ri(x,y)：通过该通路后通过该通路后y的值的值通过此路径的条件通过此路径的条件第23页/共62页3 - 243、证明检验条件：运用数学工具证明步骤、证明检验条件：运用数学工具证明步骤2得得到的所有检验条件，如果每一条通路检验条件都到的所有检验条件，如果每一条通路检验条件都为真，则该程序为部分正确的。为真，则该程序为部分正确的。第24页/共62页3 - 25实例实例设设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 y2 A (x) B P(x,y)y1 zG结束结束C (x,z)DETF F T第25页/共62页3 - 26证明证明(1)建立断言建立断言 (x)： x10 x2 0 (x,z)： z=gcd(x1,x2) 在在B点建立不变式断言点建立不变式断言P(x,y)： x10 x2 0 y10 y2 0 gcd(y1,y2)= gcd(x1,x2)(2)建立检验条件建立检验条件 通路通路1：A-B; 通路通路2：B-D-B 通路通路3：B-E-B; 通路通路4：B-G-C为每一条通过，建立检验条件为每一条通过，建立检验条件开始开始(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页3 - 27通路通路1：A-B 无条件，无条件， R1(x,y)恒真，结果恒真，结果y取值为取值为x。 检验条件为：检验条件为： (x) P(x,y) 即即 x10 x2 0 x10 x2 0 gcd(x1,x2)= gcd(x1,x2)开始开始(x1,x2) (y1,y2)y1=y2y1y2y1-y2 y1y2-y1 y2 A (x) B P(x,y)y1 zG结束结束C (x,z)DETF F T证明证明第27页/共62页3 - 28通路通路2：B-D-B R2(x,y)=y1 y2 y1y2 r2(x,y) =(y1- y2,y2) 输入输出均为输入输出均为P(x,y) 检验条件为：检验条件为： P(x,y) y1 y2 y1y2 P(x, y1- y2,y2) 将断言将断言P(x,y)代入，即得代入，即得 x10 x2 0 y10 y2 0 gcd(y1,y2)= gcd(x1,x2) y1 y2 y1y2 x10 x2 0 y1 - y2 0 y2 0 gcd(y1 - y2,y2)= gcd(x1,x2)开始开始(x1,x2) (y1,y2)y1=y2y1y2y1-y2 y1y2-y1 y2 A (x) B P(x,y)y1 zG结束结束C (x,z)DETF F T证明证明第28页/共62页3 - 29证明证明通路通路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 y2 A (x) B P(x,y)y1 zG结束结束C (x,z)DETF F T第29页/共62页3 - 30证明证明(3) 证明检验条件证明检验条件 通路通路1：x10 x2 0 x10 x2 0 gcd(x1,x2)= gcd(x1,x2) 显然显然 通路通路2： x10 x2 0 y10 y2 0 gcd(y1,y2)= gcd(x1,x2) y1 y2 y1y2 x10 x2 0 y1 - y2 0 y2 0 gcd(y1 - y2,y2)= gcd(x1,x2) 检验条件前项成立时，检验条件前项成立时， y1y2 为真，而为真，而y1 - y2 0为真为真 且且gcd(y1 - y2,y2) = gcd(y1,y2) = gcd(x1,x2) 检验条件为真检验条件为真 通路通路3： P(x,y) y1 y2 y1 y2 P(x, y1,y2 - y1) y1y2为真为真, y1- y2 0输出断言：输出断言： O(x,z):z2 x(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页3 - 32不变式断言法实例不变式断言法实例检验条件：检验条件：I R = O通路通路1：A-BI(x)= P(x,0,1,1)x0= 0 x 1=(0+1) 2 1=2*0+1通路通路2：B-D-BP(x,y1,y2,y3) y2 p(x,y1+1,y2+y3+2,y3+2) y12x y2=(y1+1)2 y3 = 2y1+1 y2 (y1+1) 2 CP(x,y1,y2,y3) y2x =O(x,y)y12x = y12x (y1+1) 2 x y2+y3+2=(y1+1+1) 2 y3+1=2(y1+1)+1证明：证明： x(y1+1)2y2+y3+2 = (y1+1)2 + 2y1 + 1+2 = (y1+2)2y3+2=2y1+1+2=2(y1+1)+1检验条件检验条件3y12 x y2=(y1+1)2 y3 = 2y1+1 y2x = y12 x(y1+1)2 证明：证明： y12 x xxx(y1+1,y3+2) (y1,y3) A (x) B P(x,y)y1 z结束C (x,z)DTF y2+y3 y2B第34页/共62页3 - 35内容线索内容线索程序正确性简介程序正确性简介程序测试程序测试程序正确性证明程序正确性证明简介简介Floyd不变式断言法不变式断言法子目标断言法子目标断言法Hoare规则公理方法规则公理方法第35页/共62页3 - 36子目标断言法子目标断言法子目标断言法与不变式断言法的主要区别是：子目标断言法与不变式断言法的主要区别是： 两种方法对循环所建立的断言不同。不变式断言描述了程两种方法对循环所建立的断言不同。不变式断言描述了程序变量序变量y的中间值与初始值之间关系，而子目标断言法描述的中间值与初始值之间关系，而子目标断言法描述的是的是y的中间值与循环终止时的最终值的中间值与循环终止时的最终值yend之间的关系。之间的关系。 两种方法进行归纳的方向不同。不变式断言沿着程序正常两种方法进行归纳的方向不同。不变式断言沿着程序正常执行的方向进行归纳，而子目标断言法则沿着相反方向进执行的方向进行归纳，而子目标断言法则沿着相反方向进行归纳。行归纳。第36页/共62页3 - 37不变式断言法不变式断言法输入断言：输入断言：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)STARTRead(x,y)x0y=xy:=y-xx yz:=ySTOPTFTFI(x,y)aP(x,y)bcO(x,y,z)deg例：设例：设x,y为正整数，求为正整数，求x,y的最大公约数的最大公约数z的程序，即的程序，即z=gcd(x,y)。第37页/共62页3 - 38子目标断言法子目标断言法(建立断言建立断言)输入断言输入断言 I(x,y):x0=0 y0=0 输出断言输出断言 O(x,y,z):z=gcd(x,y)子目标断言子目标断言 P(x,y,yend): x=0 y=0 = yend = gcd(x,y)STARTRead(x,y)x0y=xy:=y-xx yz:=ySTOPTFTFI(x,y)aP(x,y)bcO(x,y,z)deg当控制以当控制以x,y的容许值通过的容许值通过L时，时，x,y的当前值的最大公约数等于的当前值的最大公约数等于y 的最终值。的最终值。第38页/共62页3 - 39子目标断言法子目标断言法( (建立检验条件建立检验条件) )通路通路1：b-c 证明当控制最后一次通过证明当控制最后一次通过L时，即控制时，即控制转出循环时，子目标断言成立。转出循环时，子目标断言成立。检验条件检验条件1x=0 = x=0 y=0 = yend =gcd(x,y) 通路通路2：b-d-b 通过循环的通过循环的then通路之后的子目标通路之后的子目标断言蕴涵通过此通路之前的子目标断言。断言蕴涵通过此通路之前的子目标断言。检验条件检验条件2P(x,y-x, yend) x0 yx =P(x,y, yend)x=0 y-x=0 yend = gcd(x,y-x) x0 yx =x=0 y=0 yend = gcd(x,y)第39页/共62页3 - 40通路通路3：b-e-b通过循环的通过循环的else通路之后的子目标断通路之后的子目标断言蕴涵通过此通路之前的子目标断言。言蕴涵通过此通路之前的子目标断言。检验条件检验条件3P(y,x, yend) x0 y P(x,y, yend)通路通路4：a-b 证明如果输入断言为真，且当控制第一证明如果输入断言为真，且当控制第一次通过次通过L时子目标断言为真，则输出断言为真。时子目标断言为真，则输出断言为真。检验条件检验条件4x0=0 y0=0 P(x0,y0, yend)= yend = gcd(x0,y0)第40页/共62页3 - 41子目标断言法子目标断言法( (证明检验条件证明检验条件) )检验条件检验条件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) x0 yx =P(x,y, yend)即证明：即证明：x=0 y-x=0 yend = gcd(x,y-x) x0 yx =x=0 y=0 yend = gcd(x,y) 由：由： x0 yx = y0,以及以及 gcd(x,y-x) = gcd(x,y)，当，当且仅当且仅当x0,y0可知可知yend gcd(x,y-x) gcd(x,y) 第41页/共62页3 - 42内容线索内容线索程序正确性简介程序正确性简介程序测试程序测试程序正确性证明程序正确性证明简介简介Floyd不变式断言法不变式断言法子目标断言法子目标断言法Hoare规则公理方法规则公理方法第42页/共62页3 - 43公理化方法公理化方法公理化方法是由于公理化方法是由于1969年提出的一种形式化的证明年提出的一种形式化的证明程序部分正确性的方法程序部分正确性的方法第43页/共62页3 - 44一、一、whilewhile型程序型程序While型程序由一个有限的语句序列组成。每个语句之间以型程序由一个有限的语句序列组成。每个语句之间以分号隔开。分号隔开。B0;B1;Bn其中其中B0是程序中唯一的开始语句：是程序中唯一的开始语句： START yf(x) Bi是下列语句之一：是下列语句之一：（1）赋值语句：）赋值语句：y g(x,y)（2）条件语句：）条件语句：if R then F1 else F2 或者：或者： if R do F1（3）循环语句：）循环语句：while R do F1（4）复合语句：）复合语句：begin F1; F2; Fk end（5）停机语句：）停机语句：z h(x,y) HALT 第44页/共62页3 - 45二、不变式演绎系统二、不变式演绎系统1、不变式语句、不变式语句P F Q 其中其中P 和和Q是逻辑表达式，是逻辑表达式，F是一个程序段。它的含义是一个程序段。它的含义是：如果执行是：如果执行F以前以前P成立，且执行终止，则执行成立，且执行终止，则执行F后后Q成立。这时不变式语句为成立。这时不变式语句为真真。不变式语句也称为。不变式语句也称为归纳表归纳表达式。达式。2.推理规则推理规则A1, A2,An B其中其中B是一个不变式语句。是一个不变式语句。Ai(i=1,.n)是一个逻辑表达式是一个逻辑表达式或者是其他的不变式语句。它的含义是：为了推论后项或者是其他的不变式语句。它的含义是：为了推论后项B为为真，只需证明前项真，只需证明前项A1, A2,An为真。为真。第45页/共62页3 - 46为了证明不变式语句，为了证明不变式语句， Hoare定义了定义了1条赋值公理条赋值公理和和4条推理规则。条推理规则。（1）赋值公理）赋值公理 P(x,g(x,y)y g(x,y)P(x,y) (2)条件规则条件规则 S1Q和和 S2Q为表示方便，我们可用证明规则的一般形式为表示方便，我们可用证明规则的一般形式显然，上述条件语句的二种形式分别可表示为显然，上述条件语句的二种形式分别可表示为 BP BP,QSthenBifPQBPQSBP,2121QSelseSthenBifPQSBPQSBP第46页/共62页3 - 47Hoare验证系统验证系统（3）while规则规则 1) while B do S PI,I RFI,I R=Q P while R do FQ PI表示当控制进入循环时，不变式表示当控制进入循环时，不变式I为真；为真；条件条件IRFI表示表示I是不变式，即如果执行是不变式，即如果执行F前前I为真为真,且且F执行终止，则执行终止，则F执行后执行后I仍为真。仍为真。 条件条件I R=Q 表示如果控制退出循环，表示如果控制退出循环，Q将是真。将是真。第47页/共62页3 - 48Hoare验证系统验证系统4、并置规则、并置规则PF1R,RF2Q PF1;F2Q5、结论规则、结论规则 P=R,RFQ PFQ或者或者 PFR R=Q PFQ第48页/共62页3 - 49 P:trueP A0B:=AB0 B 0P A 0B:= -AB 0则，则，trueif A0 then B:=A else B=-AB 0例：例： 计算计算X=MAX(A,B)的程序为的程序为if A B then X:=A else X:=B. 试验证其正确性。试验证其正确性。 证明：证明：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页3 - 50证明程序部分正确性的公理化方法就是依据以上的几条证明程序部分正确性的公理化方法就是依据以上的几条公理和规则进行的公理和规则进行的,推理过程一般有两种形式推理过程一般有两种形式:(1)根据给出的不变式断言根据给出的不变式断言,建立一些引理建立一些引理,根据这些引理根据这些引理和赋值公理和赋值公理,对程序对程序P中的每一个赋值语句中的每一个赋值语句Fi导出相应的导出相应的不变式语句不变式语句Ri Fi Qi。再根据这些不变式语句和上述。再根据这些不变式语句和上述的四条规则逐步地组成越来越长的程序段，一直到推导的四条规则逐步地组成越来越长的程序段，一直到推导出：出： (x)P (x,z)为止。这样就证明了程序为止。这样就证明了程序P的部分的部分正确性。正确性。（2）从不变式语句）从不变式语句 (x)P (x,z)出发，利用有关的出发，利用有关的规则将它逐步分解，一直到将所有的语句推演为逻辑表规则将它逐步分解，一直到将所有的语句推演为逻辑表达式（即检验条件）。然后，证明这些逻辑表达式成达式（即检验条件）。然后，证明这些逻辑表达式成立。这样就证明了程序的部分正确性。立。这样就证明了程序的部分正确性。 第50页/共62页3 - 51例例 利用公理化方法证明例利用公理化方法证明例5.2中的程序的部分正确性中的程序的部分正确性STARTx0(y1,y2,y3)-(0,1,1)While y2x doP(x,y)(y1,y2,y3)-(y1+1,y2+y3+2,y3+2)Z0=P(x,0,1,1)引理引理5.2 P(x,y) y2Px,y1+1,y2+y3+2,y3+2引理引理5.3 P(x,y) y2x= (x,y1)(1)根据赋值公理有根据赋值公理有P(x,0,1,1)(y1,y2,y3)0(y1,y2,y3)- (0,1,1)P(x,y)(2)和和(1)类似，根据赋值公理，引理类似，根据赋值公理，引理5.2和结论规则，和结论规则，P(x,y) y2x (y1,y2,y3)x，根据，根据while规规则和（则和（2）中的结论可得：）中的结论可得：P(x,y)While y2x do(y1,y2,y3)x 第53页/共62页3 - 54（4）根据并置规则和（）根据并置规则和（1），（），（3）中的结论可得：）中的结论可得：x0(y1,y2,y3)-(0,1,1)While yx do(y1,y2,y3)x (5)根据赋值公理有：根据赋值公理有： (x,y1)zx z0(y1,y2,y3)-(0,1,1)While yx do(y1,y2,y3)-(y1+1,y2+y3+2,y3+2)Z0 y00 (x0 0 v y0 0 ) (x,y)x then y-y-x; else (s,x,y)-(x,y,s) y= gcd(x0,y0)z0 y0 (x0 0 v y0 0 ) gcd(x,y)= gcd(x0,y0)第56页/共62页3 - 57要证明程序要证明程序A的部分正确性，只需证明下面的不变的部分正确性，只需证明下面的不变式语句：式语句：Goal 1:x0 y0 (x0 0 v y0 0 )Body Ay=gcd(x0,y0)第57页/共62页3 - 58第一步；根据并置规则，为了证明第一步；根据并置规则，为了证明Goal 1，只需证，只需证明下面两个不变式语句明下面两个不变式语句Goal 2x00 y00 (x0 0 v y0 0 )（x,y）0 y0 (x0 0 v y0 0 )= P(x0,y0)根据根据while规则，为了证明规则，为了证明Goal 3，只需证明，只需证明Goal 4P(x,y) x 0 if yx then elseP(x,y)LOG 2:P(x,y) x =0= y= gcd(x0,y0)第59页/共62页3 - 60第三步：根据条件规则，为了证明第三步：根据条件规则，为了证明Goal 4，只需证明，只需证明Goal 5：P(x,y) x 0 yxy-y-xP(x,y)Goal 6:P(x,y) x 0 yx(s,x,y)x=P(x,y-x)LOG 4P(x,y) x 0 yP(y,x) 就将证明就将证明Goal1归结为证明逻辑表达式归结为证明逻辑表达式LOG1、 LOG2、 LOG3、 LOG4。这四个逻辑表达式正好是例。这四个逻辑表达式正好是例5.3中的四个检验条件，前面已经证明了他们为真。中的四个检验条件，前面已经证明了他们为真。第61页/共62页3 - 62感谢您的观看。感谢您的观看。第62页/共62页