第3章-程序的正确性证明

第三章程序的正确性证明主要内容程序的测试Floyd-Hoare规则公理方法Dijkstra最弱前置条件方法程序的正确性所谓一段程序是正确的，是指这段程序能准确无误地完成编写者所期望赋予它的功能。或者说，对任何一组允许的输入信息，程序执行后能得到一组和这组输入信息相对应的正确的输出信息。通俗地说，“做了它该做的事，没有做它不该做的事”一段程序是错误的，是指：（1）程序完成的事情并不是程序员想要完成的事情；（2）程序员想要程序完成的事情，程序并没有完成。一般来说，程序中含有错误是很难避免的。错误可能有：（1）设计时的错误；（2）程序编写时的错误；（3）运行时的错误等。发现错误或尽量减少错误，是程序设计人员的努力方向，更是其职责。如何保证程序的正确性要求1、从编程时就应该尽量地避免和减少错误的发生2、当程序编好后要尽量找出错误，纠正错误避免错误的方法

1、程序的结构要简单2、采用标准的软件设计工具、标准的算法手册以及有效的程序设计方法发现错误的方法

1、利用测试工具:跟踪程序的运行，用测试的办法去查找并发现程序错误；2、利用程序的验证系统：证明程序的正确性。程序测试：给程序一组或几组初始值进行试运行，将运行的结果与实现已知的结果比较，若两则相同，则认为程序是正确的，若两则不同，则说明程序有错误。一、程序测试软件测试的目的基于不同的立场，存在着两种完全不同的测试目的。从用户的角度出发，普遍希望通过软件测试暴露软件中隐藏的错误和缺陷，以考虑是否可接受该产品。从软件开发者的角度出发，则希望测试成为表明软件产品中不存在错误的过程，验证该软件已正确地实现了用户的要求，确立人们对软件质量的信心。程序测试1983年IEEE提出的软件工程术语中给软件测试下的定义是：“使用人工或者自动手段来运行或测定某个系统的过程，其目的在于检验它是否满足规定的需求或是弄清预期结果与实际结果之间的差别。”测试是程序的执行过程，目的在于发现错误。一个好的测试用例在于能发现至今未发现的错误；一个成功的测试是发现了至今未发现的错误的测试。测试的原则1.应当“尽早地和不断地进行软件测试”。2.测试用例应由测试输入数据和对应的预期输出结果组成。3.程序员应避免检查自己的程序。4.在设计测试用例时，应当包括合理的输入条件和不合理的输入条件。5.充分注意测试中的群集现象。即测试后程序中残存的错误数目与该程序中已发现的错误数目成正比。6.严格执行测试计划，排除测试的随意性。7.应当对每一个测试结果做全面检查。8.妥善保存测试计划，测试用例，出错统计和最终分析报告，为维护提供方便。程序测试实质上只是一种抽样检查测试过程：选取测试数据→执行程序→输入测试数据→记录执行结果→手工核对结果因此，测试只是一种查错的手段，它可以帮助人们去发现程序中的错误，但不能证明程序中没有错误，即：测试不能证明程序是正确的

程序测试的过程…软件测试方法软件测试的方法和技术是多种多样的。对于软件测试技术，根据不同角度，可以将测试方法分为不同种类。（1）从是否需要执行被测软件的角度，可以分为静态测试和动态测试；（2）从测试是否针对系统内部结构和具体实现算法的角度，可以分为白盒测试和黑盒测试；（3）从实际测试的前后过程来看，软件测试是由一系列的不同测试组成，这些步骤可以分为：单元测试、组装测试（集成测试）、确认测试和系统测试。两种重要的软件测试方法

黑盒测试这种方法是把测试对象看做一个黑盒子，测试人员完全不考虑程序内部的逻辑结构和内部特性，只依据程序的需求规格说明书，检查程序的功能是否符合它的功能说明。黑盒测试又叫做功能测试或数据驱动测试。

白盒测试此方法把测试对象看做一个透明的盒子，它允许测试人员利用程序内部的逻辑结构及有关信息，设计或选择测试用例，对程序所有逻辑路径进行测试。通过在不同点检查程序的状态，确定实际的状态是否与预期的状态一致。因此白盒测试又称为结构测试或逻辑驱动测试。黑盒测试方法是在程序接口上进行测试，主要是为了发现以下错误:是否有不正确或遗漏了的功能?在接口上，输入能否正确地接受?能否输出正确的结果?是否有数据结构错误或外部信息(例如数据文件)访问错误?性能上是否能够满足要求?是否有初始化或终止性错误?用黑盒测试发现程序中的错误，必须在所有可能的输入条件和输出条件中确定测试数据，来检查程序是否都能产生正确的输出。但这是不可能的。假设一个程序P有输入量X和Y及输出量Z。在字长为32位的计算机上运行。若X、Y取整数，按黑盒方法进行穷举测试：可能采用的测试数据组：232×232＝264

如果测试一组数据需要1毫秒，一年工作365×24小时，完成所有测试需5亿年。

软件人员使用白盒测试方法，主要想对程序模块进行如下的检查：对程序模块的所有独立的执行路径至少测试一次；对所有的逻辑判定，取“真”与取“假”的两种情况都至少测试一次；在循环的边界和运行界限内执行循环体；测试内部数据结构的有效性；对一个具有多重选择和循环嵌套的程序，不同的路径数目可能是天文数字。给出一个小程序的流程图，它包括了一个执行20次的循环。包含的不同执行路径数达520条，对每一条路径进行测试需要1毫秒，假定一年工作365×24小时，要想把所有路径测试完，需3170年。即使能完成这样的测试，也不意味差程序没有错误。如：x=x+z,错误写成x=x-z,且当z=0时，这种错误仍然难以发现

。测试常常是不充分的，它只能发现某些错误存在，而不能证明错误的不存在

。…黑盒测试

等价类划分

边界值分析

错误推测法

因果图例子某个TRIANGLE程序，用3个整数表示一个三角形的3条边长。当输入3个整数后，该程序输出一个结果，指出这三角形是等腰，等边，还是不等边三角形。这个例子只知程序的功能，而不知内部的逻辑与结构。在选择数据组来测试程序时，我们可以凭经验，考虑如下情况：1）合理构成等腰三角形2）合理构成等边三角形3）合理构成不等边三角形4）等腰三角形的三种排列5）三个正数，其中两个数之和等于第三个数6）两边之和等于第三边的三种排列7）三个正数，其中两个数之和小于第三个数8）两边之和小于第三边的三种排列9）输入三个数，其中含有010）输入三个数，其中含有负数11）输入三个数，其中含有非整数值12）输入三个均为0的数13）输入三个均为非法字符列出各种产生的情况来测试的方法显然是黑盒子方法。它不关心盒子内程序的具体逻辑，只是根据程序功能来设计测试用例等价类划分①有效等价类：是指对于程序的规格说明来说，是合理的，有意义的输入数据构成的集合。②无效等价类：是指对于程序的规格说明来说，是不合理的，无意义的输入数据构成的集合。

例如，在程序的规格说明中，对输入条件有一句话：“……项数可以从1到999……”，则有效等价类是“1≤项数≤999”两个无效等价类是“项数＜1”或“项数＞999”。在数轴上表示成:

边界值分析

人们从长期的测试工作经验得知，大量的错误是发生在输入或输出范围的边界上，而不是在输入范围的内部。因此针对各种边界情况设计测试用例，可以查出更多的错误。比如，在做三角形计算时，要输入三角形的三个边长：A、B和C。我们应注意到这三个数值应当满足

A＞0、B＞0、C＞0、A＋B＞C、A＋C＞B、B＋C＞A，才能构成三角形。但如果把六个不等式中的任何一个大于号“＞”错写成大于等于号“≥”，那就不能构成三角形。问题恰出现在容易被疏忽的边界附近。使用边界值分析方法设计测试用例，首先应确定边界情况。应当选取正好等于，刚刚大于，或刚刚小于边界的值做为测试数据，而不是选取等价类中的典型值或任意值做为测试数据。错误推测法人们也可以靠经验和直觉推测程序中可能存在的各种错误，从而有针对性地编写检查这些错误的例子。这就是错误推测法。错误推测法的基本想法是：列举出程序中所有可能有的错误和容易发生错误的特殊情况，根据它们选择测试用例。因果图如果在测试时必须考虑输入条件的各种组合，可使用一种适合于描述对于多种条件的组合，相应产生多个动作的形式来设计测试用例，这就需要利用因果图。把输入条件视为“因”，把输出条件视为“果”，将黑盒看成是从因到果的网络图，采用逻辑图的形式来表达功能说明书中输入条件的各种组合与输出的关系。根据这种关系可选择高效的测试用例。因果图是一种形式化语言，是一种组合逻辑网络图。因果图方法最终生成的就是判定表。它适合于检查程序输入条件的各种组合情况。…实例…用因果图生成测试用例的基本步骤(1)分析软件规格说明描述中，哪些是原因(即输入条件或输入条件的等价类)，哪些是结果(即输出条件)，并给每个原因和结果赋予一个标识符。(2)分析软件规格说明描述中的语义，找出原因与结果之间，原因与原因之间对应的是什么关系?根据这些关系，画出因果图。(3)由于语法或环境限制，有些原因与原因之间，原因与结果之间的组合情况不可能出现。为表明这些特殊情况，在因果图上用一些记号标明约束或限制条件。(4)把因果图转换成判定表。(5)把判定表的每一列作为依据，设计测试用例。…实例…在因果图中出现的基本符号通常在因果图中用Ci表示原因，用Ei表示结果，各结点表示状态，可取值“0”或“1”。“0”表示某状态不出现，“1”表示某状态出现。主要的原因和结果之间的关系有：…实例…表示约束条件的符号为了表示原因与原因之间，结果与结果之间可能存在的约束条件，在因果图中可以附加一些表示约束条件的符号。即a、b不能同时为1a、b中仅有一个为1a为1时，b必须为1若a为1时，则b强制为0a、b、c不能同时为0…实例…例如，有一个处理单价为5角钱的饮料的自动售货机软件测试用例的设计。其规格说明如下：若投入5角钱或1元钱的硬币，押下〖橙汁〗或〖啤酒〗的按钮，则相应的饮料就送出来。若售货机没有零钱找，则一个显示〖零钱找完〗的红灯亮，这时再投入1元硬币并押下按钮后，饮料不送出来而且1元硬币也退出来；若有零钱找，则显示〖零钱找完〗的红灯灭，在送出饮料的同时退还5角硬币。”…实例…(1)分析这一段说明，列出原因和结果原因:1.售货机有零钱找2.投入1元硬币3.投入5角硬币4.押下橙汁按钮5.押下啤酒按钮建立中间结点，表示处理中间状态11.投入1元硬币且押下饮料按钮12.押下〖橙汁〗或〖啤酒〗的按钮13.应当找5角零钱并且售货机有零钱找14.钱已付清…实例…结果：21.售货机〖零钱找完〗灯亮22.退还1元硬币23.退还5角硬币24.送出橙汁饮料25.送出啤酒饮料(2)画出因果图。所有原因结点列在左边，所有结果结点列在右边。(3)由于2与3，4与5不能同时发生，分别加上约束条件E。(4)因果图…实例……实例…(5)转换成判定表…实例程序测试的黑盒子方法常凭经验进行，在设计测试用例时可以综合使用上述各种方法。在设计测试数据时，我们应该考虑认为最易出错和最易忽略的地方，进行重点测试。…白盒测试

逻辑覆盖：以程序内部的逻辑结构为基础的设计测试用例的技术。

语句覆盖

判定覆盖

条件覆盖

判定－条件覆盖

条件组合覆盖

路径覆盖循环覆盖基本路径测试例子试测试下面这一程序ProcedureP(varA,B:REAL)beginif(A>1)and(B=0)thenX:=X/A;if(A=2)or(X>1)thenX:=X+1;end在执行这个程序时，有各种不同的路径，如：abdabedacbdacbed我们可用白盒子方法设计测试用例，其任务是尽可能多地执行各种语句，以及调试到各种路径。如选择A=2,B=0,X=3则可执行路径acbed此时能覆盖到全部2个计算框，可发现一般的语句的错误这组数据可使语句都能执行一次我们通常把这种注重语句的覆盖叫“语句覆盖”执行足够多的测试用例，使得被测程序中每个可执行语句至少被执行一次这种覆盖肯定是不充分的，如：第一个判断中and误写为or，第二个判断中X>1误写为X>0，则无法暴露出程序的错误。语句覆盖是最弱的逻辑覆盖准则。如选择A=3,B=0,X=1A=2,B=1,X=3则可执行的路径为acbdabed从所走路径来看，上面这组数据要全面一些，它不仅通过全部两个计算框，而且第一个判别框的两边都执行过一次。我们通常把这种注重选择测试的覆盖叫做“判定覆盖”，又称为“分支覆盖”。执行足够多的测试用例，使得被测程序中每个语句至少被执行一次，且每个判断的真假分支至少执行一次但这组数据仍未检查到路径abd;第一个计算框执行结果是否影响条件的执行也尚未测试到。它仍不充分如选择A=2,B=0,X=4A=1,B=1,X=1则可执行的路径为acbedabd从这组数据来看，它注意了4个条件A>1,B=0,A=2和X>1的覆盖。我们称这种注重判断的覆盖为“条件覆盖”。执行足够多的测试用例，使得被测程序中每个判定的每个条件的可能值至少执行一次虽然覆盖有所改善，但对第一个判断为真，第二个为假这一路径acbd未测试到。它仍不充分判定/条件覆盖执行足够多的测试用例，使得被测程序中的判定的每个条件的所有可能取值至少执行一次，同时每个判定本身的所有可能判定结果至少执行一次。是判定覆盖与条件覆盖的综合，但不能保证检查出逻辑表达式的全部错误。对于上例中A>1时检查B=0，而A<=1时，B<>0却不去验证了。A=2B=0X=4;A=3,B=1,X=1两个测试用例能同时满足判定、条件覆盖

以上这些数据虽然均达到一些测试目的，且各有侧重，但是都是不充分的。如从条件出发，用组合的办法使各个条件都能执行到，则我们可以写出以下8种条件组合：1)A>1,B=02)A>1,B<>0;(<>是不等号)3)A<=1,B=04)A<=1,B<>05)A=2,X>16)A=2,X<=17)A<>2,X>18)A<>2,X<=1满足条件组合覆盖必满足判定、条件、判定/条件覆盖，但仍不能遍历每条路径。根据这8种条件组合，又可以优化组成如下4组数据：A=2,B=0,X=4A=2,B=1,X=1A=1,B=0,X=2A=1,B=1,X=1它们都能使各种条件均能出现一次。虽然这个组合方法比较方便，逻辑也很清楚，且对执行条件来说还是比较全面的，但是仍然又未走遍的路径，如acbd在测试时，还要注意到计算机执行多个条件的特点，即它必须把多个条件分解为简单判别才能执行，如上述例子可分解为右图。

路径覆盖执行足够多的测试用例，使得被测程序中每条可能路径至少通过一次。上例中设计测试用例:

测试用例通过ABX路径

111abd112abed301acbd204acbed满足路径覆盖保证了每个可能的路径至少通过一次，与条件组合覆盖结合使用可能取得较好效果。从以上两个例子可以看出，测试通常是不充分的，它只能发现某些错误的存在，而不能证明错误的不存在。所以，在真正设计测试用例的过程种常常要考虑经济性，可行性。测试的关键就是如何设计好高效，可行的用例程序。程序测试工具美国MI公司开发的TestDirector产品作为测试管理流程平台，运用WinRunner和QuickTestProfessional作为自动化测试工具，推荐LoadRunner作为性能测试工具。MI公司作为一个跨国型业内专业公司，在自动化测试方面积累了丰富的经验。其测试工具作为目前测试市场的主流工具，市场占有率超过50％，从测试平台的先进性上来说，达到了国际上主流标准。

美国SEGUE公司的SILK系列自动测试技术。SILK系列自动化黑盒测试平台能够全面适应电子商务技术的最新发展，具有测试自动化，易用易维护，场景模拟精确，支持分布式测试，支持多标准协议，扩展性强等优点。

正确性证明测试只能发现程序错误，但不能证明程序无错。原因：测试并没有也不可能包含所有数据，只是选择了一些具有代表性的数据，所以它具有局限性。正确性证明是通过数学技术来确定软件是否正确，也就是说，是否符合其规格说明。正确性证明的发展二、Floyd-Hoare规则公理方法

设在程序运行之前输入一组X1，X2…Xn(断言Ｐ，也称为前断言)，经过S程序（语句）得到一组预定的Y1，Y2…Yn(断言Ｑ，也称为后断言)，则称程序S（语句）为正确的。用Hoare的记法，则为{P}S{Q}（一）基本规则

1）如果执行之前P是真，执行之后Q也是真，则记为

2）若n条路径在语句T之前汇合，则所有前面语句Si的结论Qi都必须在逻辑上蕴含语句T的前提P，就是说

其中，i=1,2,…,n.。

，，3)若断言P在条件B的判断之前成立，则判断的两个结论分别是

和4)若断言P位于赋值E于变量I之后，则P中出现的所有I替换成E，可得到赋值的前提（称赋值等效）。

5)凡蕴含一语句前提的断言，都是这个语句的前提。凡一语句结论所蕴含的断言，都是这个语句的结论。

上述规则将作为工具，对程序进行验证。

（二）简单语句的证明

1、空语句

2、赋值语句

{P}{P}结论即为前提

{}I:=E{P}由规则4直接得到其结论3、条件语句

来记，其中

是规则的前提，H是结论，它表示如果

为真，那么H也为真。

显然，上述条件语句的二种形式分别可表示为{P}ifBthenS1elseS2{Q}由规则3得到{}S1{Q}和{}S2{Q}为表示方便，我们可用证明规则的一般形式

5、分情选择语句

4、复合语句

{P}beginS1，S2，…，Snend{Q}

其中：i=1,2…,n,{Pn}={Q}L1:S1L2:S2…Ln:Snend{Q}已知：前提P为y=x2

，

D=2x-1，求顺序执行下列各语句后的结论QD:=D+2y:=y+DD:=D+2y:=y+D已知前置断言，从前往后看：{P:y=x2

，

D=2x-1}D:=D+2

y:=y+D

D:=D+2y:=y+D

例1：

y=x2，D=2x+1y=x2+2x+1，D=2x+1y=x2+2x+1，D=2x+3y=x2+4x+4，D=2x+3Q:y=(x+2)2D=2(x+2)-1已知前提P为{P:A=A0B=B0}，求执行语句后的结论QT:=AA:=BB:=T

从前往后证：{P:A=A0B=B0}

T:=A

A:=B

B:=T

例2：

（T=A0）（B=B0）（T=A0）（A=B0）（B=A0）（A=B0）从后往前证：{P:A=A0∧

B=B0}{B=B0∧A=A0}

T:=A

{B=B0∧T=A0}A:=B

{A=B0∧

T=A0}B:=T

{Q:A=B0∧

B=A0}例3：

{PA>0}B:=A{B>0}{B>=0}{PA<=0}B:=-A{B>=0}例4：

计算X=MAX(A,B)的程序为ifA>=BthenX:=AelseX:=B试验证其正确性。

证明：{P:true}{PA>=B}X:=A{X=AX>=B}{PA<B}X:=B{X=BX>A}而X=AX>=BX=MAX(A,B)X=BX>AX=MAX(A,B)

故{P:true}ifA>=BthenX:=AelseX:=B.{X=MAX(A,B)}

求如图所示条件语句的前提与结论{P:true}则，{true}ifA>0THENB:=AelseB:=-A{B>=0}6、循环语句

ρ称为循环不变式：一个在每次循环的前后均为真的谓词。

终止性：

①②{t0({0<T=t0}S{0T<t0})T(界函数)

要完全正确性证明while语句，需5步

1.

Pρ2.

{ρB}S{ρ}3.

{ρB}{Q}4.

{ρB}T>05.{T=t0}S{T<t0}1)whileBdoS

例5：

求两个自然数相除所得的商（在Q中）和余数（在R中）

{P:x>0y>0}Q:=0;R:=x;whileR>=ydobeginR:=R-y;Q:=Q+1end{Q:x=R+Q*y0<=R<yQ>=0}其中循环不变式为：{ρ:x=R+Q*yR>0Q>=0}界函数T:R

证明：(1)P={x>0y>0}Q:=0;R:=x;P1={x>0y>0Q=0R=x}(2)循环语句1.

P1ρ={x=R+Q*yR>0Q>=0}，显然成立2.

{ρB}R:=R-y;Q:=Q+1{ρ}{ρB}{x=R+Q*yR>0Q>=0R>=y}R:=R-y{x=R+y+Q*yR>0-yQ>=0R>=y-y}{x=R+(Q+1)*yR>-yQ>=0R>=0}Q:=Q+1{x=R+Q*yR>-yQ>=0R>=0}{ρ}3.

{ρB}{Q}

{x=R+Q*yR>0Q>=0R<y}{Q:x=R+Q*y0<=R<yQ>=0}4.

{ρB}T>=0{x=R+Q*yR>0Q>=0R>=y}R>=05.

{T=t0}R:=R-y;Q:=Q+1{T<t0}{R=t0}R:=R-y;{R=t0-y}Q:=Q+1{R=t0-y<t0}T<t0{ρ:x=R+Q*yR>0Q>=0}1.

Pρ2.

{ρB}S{ρ}3.

{ρB}{Q}4.

{ρB}T>05.{T=t0}S{T<t0}2)repeat

要完全正确性证明repeat语句，需5步。

1.

Pρ2.

{ρ}S{Q}3.

{QB}{ρ}4.

{QB}{R}5.

{ρB}T>06.

{T=t0}S{T<t0}例6：用加法实现乘法

{P:x>0y>0}z:=0;u:=x;repeatz:=z+y;u:=u-1;untilu=0{R:z=x*y}ρ:x*y=z+u*yu>0Q:x*y=z+u*yu>=0证明：1.{P}z:=0;u:=x;{P’}{P}z:=0;{x>0y>0z=0}u:=x;{x>0y>0z=0u=x}{P’}{x>0y>0z=0u=x}2.{P’}repeatz:=z+y;u:=u-1;untilu=0{R}1)

P’ρ显然，{x>0y>0z=0u=x}{x*y=z+u*yu>0}成立。2){ρ}z:=z+y;u:=u-1;{Q}

{x*y=z+u*yu>0}z:=z+y;{x*y=z-y+u*yu>0}u:=u-1;{x*y=z+y+(u-1)*yu>-1}{x*y=z+u*yu>-1}{Q}3){QB}{ρ}{x*y=z+u*yu>=0u<>0}{x*y=z+u*yu>0}4){QB}{R}{x*y=z+u*yu>=0u=0}{x*y=zu=0}{x*y=z}{R}5){ρB}T>0{ρB}{x*y=z+u*yu>0u<>0}}因为T=u>0,所以{ρB}T>0成立6){T=t0}z:=z+y;u:=u-1;{T<t0}{u=t0}z:=z+y;{u=t0}u:=u-1;{u=t0-1<t0}{u=t0}{u<t0+1}z:=z+y;{u-1<t0}u:=u-1;{u<t0}

ρ:x*y=z+u*y∧u>0Q:x*y=z+u*y∧u>=01.

Pρ2.

{ρ}S{Q}3.

{QB}{ρ}4.

{QB}{R}5.

{ρB}T>06.

{T=t0}S{T<t0}3)forV:=AtoBdoS

分析：{P}forV:=AtoBdoS{Q}

第一次循环：{PV=A}S{Q(A)}

以后各次循环：当V=Vi执行S以后的后置断言为Q(Vi){Q(predV)}S{Q(V)}Q(B)=Q,Q(B)Q(1)

A>B{P}={Q}(2)

A<=B则证明分析过程每步成立(3)

不需证明终止性，因为FOR语句一定会终止的。{给定数组X,Y}begins:=0;{P:给定数组X,Ys=0}forI=1toNdoS:=S+X[I]*Y[I]end{Q:S=}证明：(1)

N<1{P:给定数组X,Ys=0}{Q:S=}所以，N<1是语句成立(2)

N>=1a)

{PI=1}S{Q(1)}{S=0I=1}S:=S+X[I]*Y[I]{S=}b)

{Q(pred(I))}S{Q(I)},{Q(I-1)}S{Q(I)}{S=}S:=S+X[I]*Y[I]{S=+X[I]*Y[I]}{S=}C)Q(B)=Q,Q(B)Q要证Q(B)=Q(N)=Q,即I=N,Q(N)==Q定义：假定S是一个语句，R是一个谓词，它描述S执行后所确定的某种关系。从S和R定义另外一个谓词，记为wp(“S”,R),它表示：

“所有这样的状态的集合，S从其中任一状态开始执行必将在有限的时间内终止于满足R的状态”。称wp(“S”,R)是语句S关于R的最弱前置谓词

-----------------S---------------终止{wp(“S”,R)}{R}一些状态集合后置条件三、Dijkstra最弱前置条件方法

（二）最弱前置谓词的几个性质公理

1、排奇律：wp(“S”,F)=F

要从某个状态集的任何一个状态出发执行S后必定会终止，终止时满足F，即使F为真，这样的状态是找不到的，因此对应的状态集为空。

2、合取分配律：wp(“S”,Q)wp(“S”,R)=wp(“S”,QR)表示从某一状态开始执行S，能终止，且分别满足Ｑ和Ｒ的状态，那它当然也能终止，且满足Ｑ∧Ｒ的状态，反之亦然。

3、单调律：如果QR，则wp(“S”,Q)wp(“S”,R)4、折取分配律：wp(“S”,Q)wp(“S”,R)wp(“S”,QR)确定程序：从某一个状态出发，程序不管执行多少次，所经过的路径相同，所得的结果也相同。wp(“S”,Q)∨

wp(“S”,R)=wp(“S”,Q∨R)不确定程序：从某一个状态出发，程序的任何两次执行可能得到的结果都不同，有时即便所得的结果相同，可能经过的路径也不同。wp(“S”,Q)∨

wp(“S”,R)

wp(“S”,Q∨R)

例：抛硬币具有不确定性wp(“抛硬币”，正面)=Fwp(“抛硬币”，反面)=Fwp(“抛硬币”，正面反面)=T

（三）求解最弱前置谓词的规则

1、skip、abort、复合语句wp(“skip”,R)=R(相当于空语句)wp(“abort”,R)=F(执行过程中夭折的语句)wp(“S1,S2”,R)=wp(“S1”,wp(“S2”,R))（相当于顺序复合语句）例如wp(“skip;skip”,R)=wp(“skip”,wp(“skip”,R))=R2、赋值语句(1)单个简单变量的赋值语句(2)多个简单变量的赋值语句(3)单个数组元素的赋值（1）单个简单变量的赋值语句

S::=I:=E其语义为：

wp(“I:=E”,R)=domain(E)canddomain(E)表示能获得正常表达式E结果条件。

当条件显然时，可略去此项。表示表达式E去替换R中所有自由出现的变量I。B1candB2表示从左到右的次序计算，B1为F时，则不必计算B2,其结果全为F。B1为T时，则其结果为B2的结果。B1无定义时，其结果也无定义。1.wp(“x:=x+1”,x<0)=(x+1<0)=x<-12.wp(“x:=5”,x=5)=5=5=T3.wp(“x:=5”,x≠5)=5≠5=F4.wp(“x:=A÷B”,P(x))=(B≠0)candP(A÷B)5.wp(“x:=x*x”,x4=10)=((x*x)4=10)=x8=106.设数组B的下标域为0：100，则:wp(“x:=B[I]”,x=B[I])=(0<=I<=100)candB[I]=B[I]=0<=I<=100练习7：wp(“t:=x;x:=y;y:=t”,x=X∧y=Y)=wp(“t:=x;x:=y”,wp(“y:=t”,x=X∧y=Y))=wp(“t:=x;x:=y”,x=X∧t=Y)=wp(“t:=x”,wp(“x:=y”,x=X∧t=Y))=wp(“t:=x”,y=X∧t=Y)=y=X∧x=Y(2)多个简单变量的赋值语句8.wp(“x,y:=x-y,y-x,”,x+y=c)=(x-y+y-x=c)=0=c9.wp(“s,i:=s+b[i],i+1”,i>0^s=(∑j:0<=j<i:b[j]))=i+1>0^s+b[i]=(∑j:0<=j<i+1:b[j])=i>=0^s=(∑j:0<=j<i:b[j])10.{T}a:=a+1;b:=x{a=b}wp(“a:=a+1;b:=x”,a=b)=wp(“a:=a+1”,a=x)=a+1=x11.wp(“a:=a+1;b:=x(a,b)”,a=b)=wp(“a:=a+1”,a=x(a,b))=a+1=x(a+1,b)练习(3)单个数组元素的赋值语句对一个数组元素的赋值语句S::=b[i]:=E其中b是数组名，i是b的下标表达式我们用（b;i:E)表示一个数组函数，定义为：(b;i:E)[j]=E当i=jb[j]当i≠j这样，语句b[i]:=E等价于b:=(b;i:E)若略去domain(E)与domain(i)等因素，数组的赋值语句语义是wp(“b[i]:=E”,R)=Rb(b;i:E)其中Rb(b;i:E)表示用数组(b;i;E)去替换R中自由出现的数组名b练习12.wp(“b[i]:=5”,b[i]=5)=(b[i]=5)b(b;i:5)定义=(b;i:5)[i]=5替换=5=5=T13.wp(“b[i]:=5”,b[i]=b[j])=(b[i]=b[j])b(b;i:5)定义=(b;i:5)[i]=(b;i:5)[j]替换=(i≠j^5=b[j])∨(i=j^5=5)=(i≠j^5=b[j])∨(i=j)=(i≠j∨i=j)^(5=b[j]∨i=j)=T^(i=j∨b[j]=5)=i=j∨b[j]=514.wp(“b[b[i]]:=i”,b[i]=i)=(b[i]=i)b(b;b[i]:i)

(定义)=(b;b[i]:i)[i]=i(替换)=(b[i]≠i∧b[i]=i)∨(b[i]=i∧i=i)=F∨(b[i]=i∧T)=b[i]=i3、条件语句条件语句是任何一种高级语言中不可缺少的语句之一，常用if表示。大家已熟知，它一般有二种格式，即：

ifx≥0thenZ:=xelseZ:=-x

ifx<0thenZ:=-x为说明方便，我们可改写成

ifx≥0→Z:=x

□x<0→Z:=―xfi与ifx≥0→skip□x<