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

1、第三章第三章 程序的正确性证明程序的正确性证明 主要内容主要内容程序的测试程序的测试Floyd-Hoare规则公理方法规则公理方法Dijkstra 最弱前置条件方法最弱前置条件方法程序的正确性程序的正确性所谓一段程序是正确的，是指这段程序能准确无误所谓一段程序是正确的，是指这段程序能准确无误地完成编写者所期望赋予它的功能。地完成编写者所期望赋予它的功能。或者说，对任何一组允许的输入信息，程序执行后能或者说，对任何一组允许的输入信息，程序执行后能得到一组和这组输入信息相对应的正确的输出信息。得到一组和这组输入信息相对应的正确的输出信息。通俗地说，通俗地说，“做了它该做的事，没有做它不该做的做了它

2、该做的事，没有做它不该做的事事”一段程序是错误的，是指：一段程序是错误的，是指：（1 1）程序完成的事情并不是程序员想要完成的事）程序完成的事情并不是程序员想要完成的事情；情；（2 2）程序员想要程序完成的事情，程序并没有完）程序员想要程序完成的事情，程序并没有完成。成。一般来说，程序中含有错误是很难避免的。一般来说，程序中含有错误是很难避免的。错误可能有：错误可能有：（1 1）设计时的错误；）设计时的错误；（2 2）程序编写时的错误；）程序编写时的错误；（3 3）运行时的错误等。）运行时的错误等。发现错误或尽量减少错误，是程序设计人员的努力发现错误或尽量减少错误，是程序设计人员的努力方向，更

3、是其职责。方向，更是其职责。如何保证程序的正确性如何保证程序的正确性要求要求1 1、从编程时就应该尽量地避免和减少错误的发生、从编程时就应该尽量地避免和减少错误的发生2 2、当程序编好后要尽量找出错误，纠正错误、当程序编好后要尽量找出错误，纠正错误避免错误的方法避免错误的方法 1 1、程序的结构要简单、程序的结构要简单 2 2、采用标准的软件设计工具、标准的算法手册以及有效、采用标准的软件设计工具、标准的算法手册以及有效的程序设计方法的程序设计方法发现错误的方法发现错误的方法 1 1、利用测试工具、利用测试工具: :跟踪程序的运行，用测试的办法去查找跟踪程序的运行，用测试的办法去查找并发现程序

4、错误；并发现程序错误； 2 2、利用程序的验证系统：证明程序的正确性。、利用程序的验证系统：证明程序的正确性。程序测试：给程序一组或几组初始值进行试运行，程序测试：给程序一组或几组初始值进行试运行，将运行的结果与实现已知的结果比较，若两则相将运行的结果与实现已知的结果比较，若两则相同，则认为程序是正确的，若两则不同，则说明程同，则认为程序是正确的，若两则不同，则说明程序有错误。序有错误。一、程序测试一、程序测试程序测试程序测试19831983年年IEEEIEEE提出的软件工程术语中给软件测试下的定提出的软件工程术语中给软件测试下的定义是：义是：“使用人工或者自动手段来运行或测定某个系使用人工或

5、者自动手段来运行或测定某个系统的过程，其目的在于检验它是否满足规定的需求或统的过程，其目的在于检验它是否满足规定的需求或是弄清预期结果与实际结果之间的差别。是弄清预期结果与实际结果之间的差别。”测试是程序的执行过程，目的测试是程序的执行过程，目的在于发现错误在于发现错误。一个好的测试用例在于能发现至今未发现的错误；一个好的测试用例在于能发现至今未发现的错误； 一个成功的测试是发现了至今未发现的错误的测一个成功的测试是发现了至今未发现的错误的测试。试。测试的原则1. 应当 “尽早地和不断地进行软件测试” 。2. 测试用例应由测试输入数据和对应的预期输出结果组成。3. 程序员应避免检查自己的程序。

6、4. 在设计测试用例时，应当包括合理的输入条件和不合理的输入条件。5. 充分注意测试中的群集现象。即测试后程序中残存的错误数目与该程序中已发现的错误数目成正比。6. 严格执行测试计划，排除测试的随意性。7. 应当对每一个测试结果做全面检查。8. 妥善保存测试计划，测试用例，出错统计和最终分析报告，为维护提供方便。程序测试实质上只是一种抽样检查程序测试实质上只是一种抽样检查测试过程：测试过程： 选取测试数据选取测试数据 执行程序执行程序 输入输入测试数据测试数据 记录执行结果记录执行结果 手工核对结果手工核对结果 因此，测试只是一种查错的手段，它可以帮助人们因此，测试只是一种查错的手段，它可以帮

7、助人们去发现程序中的错误，但不能证明程序中没有错去发现程序中的错误，但不能证明程序中没有错误，即：误，即：测试不能证明程序是正确的测试不能证明程序是正确的 程序测试的过程程序测试的过程软件测试方法软件测试方法软件测试的方法和技术是多种多样的。对于软件测软件测试的方法和技术是多种多样的。对于软件测试技术，根据不同角度，可以将测试方法分为不同试技术，根据不同角度，可以将测试方法分为不同种类。种类。（1）从是否需要执行被测软件的角度，可以分为）从是否需要执行被测软件的角度，可以分为静静态测试态测试和和动态测试动态测试；（2）从测试是否针对系统内部结构和具体实现算法）从测试是否针对系统内部结构和具体实

8、现算法的角度，可以分为的角度，可以分为白盒测试白盒测试和和黑盒测试黑盒测试；（3）从实际测试的前后过程来看，软件测试是由一）从实际测试的前后过程来看，软件测试是由一系列的不同测试组成，这些步骤可以分为：系列的不同测试组成，这些步骤可以分为：单元测单元测试试、组装测试（集成测试）组装测试（集成测试）、确认测试确认测试和和系统测系统测试试。两种重要的软件测试方法两种重要的软件测试方法 黑盒测试黑盒测试这种方法是把测试对象看做一个黑盒子，测试人员完这种方法是把测试对象看做一个黑盒子，测试人员完全不考虑程序内部的逻辑结构和内部特性，只依据程全不考虑程序内部的逻辑结构和内部特性，只依据程序的需求规格说明

9、书，检查程序的功能是否符合它的序的需求规格说明书，检查程序的功能是否符合它的功能说明。功能说明。黑盒测试又叫做黑盒测试又叫做功能测试功能测试或或数据驱动测试数据驱动测试。 白盒测试白盒测试此方法把测试对象看做一个透明的盒子，它允许测试此方法把测试对象看做一个透明的盒子，它允许测试人员利用程序内部的逻辑结构及有关信息，设计或选人员利用程序内部的逻辑结构及有关信息，设计或选择测试用例，对程序所有逻辑路径进行测试。择测试用例，对程序所有逻辑路径进行测试。通过在不同点检查程序的状态，确定实际的状态是否通过在不同点检查程序的状态，确定实际的状态是否与预期的状态一致。因此白盒测试又称为与预期的状态一致。因

10、此白盒测试又称为结构测试结构测试或或逻辑驱动测试逻辑驱动测试。黑盒测试方法是在程序接口上进行测试，主要是为了发现以下黑盒测试方法是在程序接口上进行测试，主要是为了发现以下错误错误: : 是否有不正确或遗漏了的功能是否有不正确或遗漏了的功能? ? 在接口上，输入能否正确地接受在接口上，输入能否正确地接受? ? 能否输出正确的结果能否输出正确的结果? ? 是否有数据结构错误或外部信息是否有数据结构错误或外部信息( (例如数据文件例如数据文件) )访问错访问错误误? ? 性能上是否能够满足要求性能上是否能够满足要求? ? 是否有初始化或终止性错误是否有初始化或终止性错误? ?用黑盒测试发现程序中的错

11、误，必须在所有可能的输入条件和用黑盒测试发现程序中的错误，必须在所有可能的输入条件和输出条件中确定测试数据，来检查程序是否都能产生正确的输输出条件中确定测试数据，来检查程序是否都能产生正确的输出。出。但这是不可能的。但这是不可能的。假设一个程序假设一个程序P P有输入量有输入量X X和和Y Y及输出量及输出量Z Z。在字长为。在字长为3232位的计位的计算机上运行。若算机上运行。若X X、Y Y取整数，按黑盒方法进行穷举测试：取整数，按黑盒方法进行穷举测试：可能采用的测试数据组：可能采用的测试数据组： 2 232322 232322 26464 如果测试一组数据需要如果测试一组数据需要1 1毫

12、秒，一年工作毫秒，一年工作3653652424小时，小时，完成所有测试需完成所有测试需5 5亿年。亿年。软件人员使用白盒测试方法，主要想对程序模块进行软件人员使用白盒测试方法，主要想对程序模块进行如下的检查：如下的检查：对程序模块的所有独立的执行路径至少测试一对程序模块的所有独立的执行路径至少测试一次；次；对所有的逻辑判定，取对所有的逻辑判定，取“真真”与取与取“假假”的两种的两种情况都至少测试一次；情况都至少测试一次；在循环的边界和运行界限内执行循环体；在循环的边界和运行界限内执行循环体；测试内部数据结构的有效性；测试内部数据结构的有效性；对一个具有多重选择和循环嵌套的程序，不同的路径数目可

13、能是天文数字。给出一个小程序的流程图，它包括了一个执行20次的循环。包含的不同执行路径数达520条，对每一条路径进行测试需要1毫秒，假定一年工作365 24小时，要想把所有路径测试完，需3170年。即使能完成这样即使能完成这样的测试，也不意的测试，也不意味差程序没有错味差程序没有错误。如：误。如：x=x+z,错误写成错误写成x=x-z,且且当当z=0时，这种错时，这种错误仍然难以发误仍然难以发现现 。测试常常是不充分的，它只能测试常常是不充分的，它只能发现某些错误存在，而不能证发现某些错误存在，而不能证明错误的不存在明错误的不存在 。黑盒测试黑盒测试 等价类划分 边界值分析 错误推测法 因果图

14、例子例子 某个某个TRIANGLETRIANGLE程序，用程序，用3 3个整数表示一个三角个整数表示一个三角形的形的3 3条边长。当输入条边长。当输入3 3个整数后，该程序输出一个整数后，该程序输出一个结果，指出这三角形是等腰，等边，还是不等个结果，指出这三角形是等腰，等边，还是不等边三角形。边三角形。这个例子只知程序的功能，而不知内部的逻辑与结这个例子只知程序的功能，而不知内部的逻辑与结构。在选择数据组来测试程序时，我们可以凭经构。在选择数据组来测试程序时，我们可以凭经验，考虑如下情况：验，考虑如下情况：1 1）合理构成等腰三角形）合理构成等腰三角形2 2）合理构成等边三角形）合理构成等边三

15、角形3 3）合理构成不等边三角形）合理构成不等边三角形4 4）等腰三角形的三种排列）等腰三角形的三种排列5 5）三个正数，其中两个数之和等于第三个数）三个正数，其中两个数之和等于第三个数6 6）两边之和等于第三边的三种排列）两边之和等于第三边的三种排列7 7）三个正数，其中两个数之和小于第三个数）三个正数，其中两个数之和小于第三个数8 8）两边之和小于第三边的三种排列）两边之和小于第三边的三种排列9）输入三个数，其中含有）输入三个数，其中含有010）输入三个数，其中含有负数）输入三个数，其中含有负数11）输入三个数，其中含有非整数值）输入三个数，其中含有非整数值12）输入三个均为）输入三个均为

16、0的数的数13）输入三个均为非法字符）输入三个均为非法字符列出各种产生的情况来测试的方法显然是黑盒子列出各种产生的情况来测试的方法显然是黑盒子方法。它不关心盒子内程序的具体逻辑，只是根方法。它不关心盒子内程序的具体逻辑，只是根据程序功能来设计测试用例据程序功能来设计测试用例等价类划分等价类划分 有效等价类：是指对于程序的规格说明来说，是合理的，有效等价类：是指对于程序的规格说明来说，是合理的，有意义的输入数据构成的集合。有意义的输入数据构成的集合。 无效等价类：是指对于程序的规格说明来说，是不合理无效等价类：是指对于程序的规格说明来说，是不合理的，无意义的输入数据构成的集合。的，无意义的输入数

17、据构成的集合。 例如，在程序的规格说明中，对输入条件有一句话：例如，在程序的规格说明中，对输入条件有一句话： “ 项数可以从项数可以从1到到999 ” ，则，则有效等价类是有效等价类是“1项数项数999”两个无效等价类是两个无效等价类是“项数项数1”或或“项数项数999”。在数轴上表示成在数轴上表示成: 边界值分析边界值分析人们从长期的测试工作经验得知，人们从长期的测试工作经验得知，大量的错误是发生在输大量的错误是发生在输入或输出范围的边界上，而不是在输入范围的内部入或输出范围的边界上，而不是在输入范围的内部。因此。因此针对各种边界情况设计测试用例，可以查出更多的错误。针对各种边界情况设计测试

18、用例，可以查出更多的错误。比如，在做三角形计算时，要输入三角形的三个边长：比如，在做三角形计算时，要输入三角形的三个边长：A、B和和C。 我们应注意到这三个数值应当满足我们应注意到这三个数值应当满足 A0、B0、C0、 ABC、ACB、BCA，才能才能构成三角形。但如果把六个不等式中的任何一个大于号构成三角形。但如果把六个不等式中的任何一个大于号“”错写成大于等于号错写成大于等于号“”，那就不能构成三角形。问题恰出现在，那就不能构成三角形。问题恰出现在容易被疏忽的边界附近。容易被疏忽的边界附近。使用边界值分析方法设计测试用例，首先应确定边界情况。使用边界值分析方法设计测试用例，首先应确定边界情

19、况。应当应当选取正好等于，刚刚大于，或刚刚小于边界的值做为测试数据选取正好等于，刚刚大于，或刚刚小于边界的值做为测试数据，而不是选取等价类中的典型值或任意值做为测试数据。而不是选取等价类中的典型值或任意值做为测试数据。错误推测法错误推测法因果图因果图如果在测试时必须考虑如果在测试时必须考虑输入条件的各种组合输入条件的各种组合，可使用，可使用一种适合于描述对于多种条件的组合，相应产生多个动一种适合于描述对于多种条件的组合，相应产生多个动作的形式来设计测试用例，这就需要利用因果图。作的形式来设计测试用例，这就需要利用因果图。把输入条件视为把输入条件视为“因因”，把输出条件视为，把输出条件视为“果果

20、”，将，将黑盒看成是从因到果的网络图，采用逻辑图的形式来表黑盒看成是从因到果的网络图，采用逻辑图的形式来表达功能说明书中输入条件的各种组合与输出的关系。根达功能说明书中输入条件的各种组合与输出的关系。根据这种关系可选择高效的测试用例。据这种关系可选择高效的测试用例。因果图是一种形式化语言，是一种组合逻辑网络图。因果图是一种形式化语言，是一种组合逻辑网络图。因果图方法最终生成的就是判定表。它适合于检查程因果图方法最终生成的就是判定表。它适合于检查程序输入条件的各种组合情况。序输入条件的各种组合情况。实例实例用因果图生成测试用例的基本步骤(1) 分析软件规格说明描述中，哪些是原因 (即输入条件或输

21、入条件的等价类)，哪些是结果 (即输出条件)，并给每个原因和结果赋予一个标识符。(2) 分析软件规格说明描述中的语义，找出原因与结果之间，原因与原因之间对应的是什么关系? 根据这些关系，画出因果图。(3) 由于语法或环境限制，有些原因与原因之间，原因与结果之间的组合情况不可能出现。为表明这些特殊情况，在因果图上用一些记号标明约束或限制条件。(4) 把因果图转换成判定表。(5) 把判定表的每一列作为依据，设计测试用例。实例实例在因果图中出现的基本符号通常在因果图中用Ci表示原因，用Ei表示结果，各结点表示状态，可取值“0”或“1”。“0”表示某状态不出现，“1”表示某状态出现。主要的原因和结果之

22、间的关系有：实例实例表示约束条件的符号为了表示原因与原因之间，结果与结果之间可能存在的约束条件，在因果图中可以附加一些表示约束条件的符号。实例实例例如，有一个处理单价为5角钱的饮料的自动售货机软件测试用例的设计。其规格说明如下：若投入5角钱或1元钱的硬币，押下橙汁或啤酒的按钮，则相应的饮料就送出来。若售货机没有零钱找，则一个显示零钱找完的红灯亮，这时再投入1元硬币并押下按钮后，饮料不送出来而且1元硬币也退出来；若有零钱找，则显示零钱找完的红灯灭，在送出饮料的同时退还5角硬币。”实例实例(1) 分析这一段说明，列出原因和结果原因: 1. 售货机有零钱找2. 投入1元硬币3. 投入5角硬币4. 押

23、下橙汁按钮5. 押下啤酒按钮建立中间结点，表示处理中间状态11. 投入1元硬币且押下饮料按钮12. 押下橙汁或啤酒的按钮13. 应当找5角零钱并且售货机有零钱找14. 钱已付清实例实例结果： 21. 售货机零钱找完灯亮22. 退还1元硬币23. 退还5角硬币24. 送出橙汁饮料25. 送出啤酒饮料(2) 画出因果图。所有原因结点列在左边，所有结果结点列在右边。(3) 由于 2 与 3 ，4 与 5 不能同时发生，分别加上约束条件E。(4) 因果图实例实例实例实例(5) 转换成判定表实例实例程序测试的黑盒子方法常凭程序测试的黑盒子方法常凭经验经验进行，在设计进行，在设计测试用例时可以综合使用上述

24、各种方法。在设测试用例时可以综合使用上述各种方法。在设计测试数据时，我们应该考虑认为最易出错和计测试数据时，我们应该考虑认为最易出错和最易忽略的地方，进行重点测试。最易忽略的地方，进行重点测试。白盒测试白盒测试 逻辑覆盖： 语句覆盖 判定覆盖 条件覆盖 判定条件覆盖 条件组合覆盖 路径覆盖循环覆盖基本路径测试例子例子试测试下面这一程序试测试下面这一程序Procedure P(varProcedure P(var A,B:REAL) A,B:REAL)beginbegin if(A if(A1)and(B=0)then X:=X/A;1)and(B=0)then X:=X/A; if(A if(

25、A=2)or (X1)then X:=X+1;=2)or (X1)then X:=X+1;endend在执行这个程序时，有各种不同的路径，如： a b d a b e d a c b d a c b e d我们可用白盒子方法设计测试用例，其任务是我们可用白盒子方法设计测试用例，其任务是尽尽可能多地执行各种语句可能多地执行各种语句，以及调试到各种路径。，以及调试到各种路径。如选择如选择 A = 2 ,B = 0 ,X = 3则可执行路径则可执行路径 a c b e d此时能覆盖到全部此时能覆盖到全部2个计算框，可发现一般的语句个计算框，可发现一般的语句的错误的错误这组数据可使语句都能执行一次这组

26、数据可使语句都能执行一次我们通常把这种我们通常把这种注重语句注重语句的覆盖叫的覆盖叫“语句覆盖语句覆盖”执行足够多的测试用例，使得被测程序中每个可执行足够多的测试用例，使得被测程序中每个可执行语句至少被执行一次执行语句至少被执行一次这种覆盖肯定是不充分的，如：第这种覆盖肯定是不充分的，如：第一个判断中一个判断中and误写为误写为or，第二个判，第二个判断中断中X1误写为误写为X0，则无法暴露出，则无法暴露出程序的错误。程序的错误。语句覆盖是最弱的逻辑覆盖准则语句覆盖是最弱的逻辑覆盖准则 。如选择如选择A = 3,B = 0,X = 1A = 2,B = 1,X = 3则可执行的路径为则可执行的

27、路径为 a c b d a b e d从所走路径来看，上面这组数据要全面一些，它不仅通从所走路径来看，上面这组数据要全面一些，它不仅通过全部两个计算框，而且第一个判别框的两边都执行过过全部两个计算框，而且第一个判别框的两边都执行过一次。一次。我们通常把这种我们通常把这种注重选择测试注重选择测试的覆盖叫做的覆盖叫做“判定覆判定覆盖盖”，又称为，又称为“分支覆盖分支覆盖”。执行足够多的测试用例，使得被测程序中每个语句至少执行足够多的测试用例，使得被测程序中每个语句至少被执行一次，且每个判断的真假分支至少执行一次被执行一次，且每个判断的真假分支至少执行一次n但这组数据仍未检查到路径但这组数据仍未检查

28、到路径abd;第一个计第一个计算框执行结果是否影响条件的执行也尚未算框执行结果是否影响条件的执行也尚未测试到。测试到。n它仍不充分它仍不充分如选择如选择A=2,B=0,X=4A=2,B=0,X=4A=1,B=1,X=1A=1,B=1,X=1则可执行的路径为则可执行的路径为 a c b e da c b e d a b d a b d从这组数据来看，它从这组数据来看，它注意了注意了4 4个条件个条件A1,B=0,A=2A1,B=0,A=2和和X1X1的覆盖。我们称这种注重的覆盖。我们称这种注重判断的覆盖为判断的覆盖为“条件覆盖条件覆盖”。执行足够多的测试用例，使得被测程序中执行足够多的测试用例，

29、使得被测程序中每个判定的每个条件的可能值每个判定的每个条件的可能值至少执行一至少执行一次次n虽然覆盖有所改善，但对第一个判断为虽然覆盖有所改善，但对第一个判断为真，第二个为假这一路径真，第二个为假这一路径acbd未测试到。未测试到。n它仍不充分它仍不充分 判定判定/ /条件覆盖条件覆盖执行足够多的测试用例，使得被测程序中的判定的执行足够多的测试用例，使得被测程序中的判定的每个条件的所有可能取值至少执行一次，同时每个每个条件的所有可能取值至少执行一次，同时每个判定本身的所有可能判定结果至少执行一次。判定本身的所有可能判定结果至少执行一次。是判定覆盖与条件覆盖的综合，但不能保证检查出是判定覆盖与条

30、件覆盖的综合，但不能保证检查出逻辑表达式的全部错误。逻辑表达式的全部错误。 对于上例中对于上例中A1A1时检查时检查B=0B=0，而，而 A=1A=1时，时，B0B0却却不去验证了。不去验证了。A=2 B=0 X=4 ; A=3,B=1,X=1两个测试用例能同时满足判定、条件两个测试用例能同时满足判定、条件覆盖覆盖 以上这些数据虽然均达到一些测试目的，且各有侧重，但是以上这些数据虽然均达到一些测试目的，且各有侧重，但是都是不充分的。都是不充分的。如从条件出发，用组合的办法使如从条件出发，用组合的办法使各个条件都能执行到各个条件都能执行到，则我，则我们可以写出以下们可以写出以下8种条件组合：种条

31、件组合：1)A1,B=02)A1,B0;(是不等号是不等号)3)A=1,B=04)A=1,B05)A=2,X16)A=2,X=17)A2,X18)A2,X0B:=AB0 B=0P A=0例例4： 计算计算X=MAX(A,B)X=MAX(A,B)的程序为的程序为if A=B then X:=A else X:=Bif 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 e

32、lse X:=B. X=MAX(A,B) 求如图所示条件语句的前提与结论求如图所示条件语句的前提与结论P:true则，则，trueif A0 THEN B:=A else B:=-AB=06 6、循环语句、循环语句 BSdoBwhileSB;QSdoBwhilePQBSBP称为称为循环不变式循环不变式：一个在每次循环的前后均为真的谓词。 终止性终止性： t t0 0(0T=t(0T=t0 0S0S0 Tt T0 5. T=t0 S T0 y0Q:=0;R:=x;while R=y do begin R:=R-y;Q:=Q+1 endQ:x=R+Q*y 0=R=0其中循环不变式为：:x=R+Q*

33、y R0 Q=0 界函数T:R 证明：(1) P=x0 y0 Q:=0;R:=x; P1=x0 y0 Q=0 R=x(2)(2)循环语句1. P1 =x=R+Q*y R0 Q=0，显然成立2. B R:=R-y; Q:=Q+1 B x=R+Q*y R0 Q=0 R=y R:=R-y x=R+y+Q*y R 0-y Q=0 R =y-y x=R+(Q+1)*y R-y Q=0 R=0 Q:=Q+1 x=R+Q*y R-y Q=0 R=0 3. B Q x=R+Q*y R0 Q=0 Ry Q:x=R+Q*y 0=R=04. B T=0 x=R+Q*y R0 Q=0 R=y R=05. T=t0 R

34、:=R-y; Q:=Q+1Tt0 R=t0 R:=R-y; R=t0-y Q:=Q+1R=t0-y t0 T0 Q=01. P 2. B S3. B Q4. B T0 5. T=t0 S T06. T=t0 S T0 y0z:=0;u:=x;repeat z:=z+y; u:=u-1;until u=0R:z=x*y: x*y=z+u*y u0Q: x*y=z+u*y u=0证明：1. P z:=0;u:=x;P P z:=0;x0 y0 z=0u:=x; x0 y0 z=0 u=x P x0 y0 z=0 u=x2.P repeat z:=z+y; u:=u-1;until u=0 R 1)

35、 P 显然， x0 y0 z=0 u=x x*y=z+u*y u0成立。2) z:=z+y; u:=u-1;Q x*y=z+u*y u0z:=z+y; x*y=z-y +u*y u0 u:=u-1; x*y=z+y +(u-1)*y u-1 x*y=z +u*y u-1 Q3)Q B x*y=z+u*y u=0 u0 x*y=z+u*y u04)Q B Rx*y=z+u*y u=0 u=0 x*y=z u=0 x*y=z R5) B T0 B x*y=z+u*y u0 u0因为T=u0,所以 B T0成立6)T=t0 z:=z+y; u:=u-1;Tt0 u=t0 z:=z+y; u=t0u:

36、=u-1; u=t0-1t0 u=t0 u t0+1 z:=z+y; u-1 t0u:=u-1;u0 Q: x*y=z+u*y u=01. P 2. SQ3. Q B 4. Q B R5. B T06. T=t0 S TB P=Q (2) A=B 则证明分析过程每步成立 (3) 不需证明终止性，因为FOR语句一定会终止的。 给定数组X,Y begin s:=0; P: 给定数组X,Y s=0 for I=1 to N do S:=S+XI*YI endNjjYjX1*Q:S= 证明：(1) N1 P: 给定数组X,Y s=0 Q:S= 所以，N=1a) P I=1SQ(1) S=0 I=1 S

37、:=S+XI*YIS= b) Q(pred(I)SQ(I), Q(I-1)SQ(I) S= S:=S+XI*YI S= +XI*YI S= C) Q(B)=Q, Q(B) Q要证Q(B)=Q(N)=Q,即I=N, Q(N)= =QNjjYjX1*0)*:1 :(jYjXNjj11*jjYjX11*IjjYjX11*IjjYjXIjjYjX1*NjjYjX1*定义定义：假定：假定S是一个语句，是一个语句，R是一个谓词，它描述是一个谓词，它描述S执执行后所确定的某种关系。从行后所确定的某种关系。从S和和R定义另外一个谓定义另外一个谓词，记为词，记为 wp(“S”,R),它表示：它表示： “所有这样

38、的状态的集合，所有这样的状态的集合，S S从其中任一状态开始从其中任一状态开始执行必将在有限的时间内终止于满足执行必将在有限的时间内终止于满足R R的状态的状态”。 称称 wp( “S”,R) 是语句是语句S关于关于R的最弱前置谓词的最弱前置谓词 - S - 终止终止 wp (“S”,R) R 一些状态集合一些状态集合 后置条件后置条件三、三、DijkstraDijkstra最弱前置条件方法最弱前置条件方法 （二）（二） 最弱前置谓词的几个性质公理最弱前置谓词的几个性质公理 1、排奇律：wp (“S”, F)=F 要从某个状态集的任何一个状态出发执行要从某个状态集的任何一个状态出发执行S后必定

39、会终后必定会终止，终止时满足止，终止时满足F，即使，即使F为真，这样的状态是找不到的，为真，这样的状态是找不到的，因此对应的状态集为空。因此对应的状态集为空。 2、合取分配律：wp(“S”,Q) wp(“S”,R)=wp(“S”, Q R) 表示从某一状态开始执行表示从某一状态开始执行S S，能终止，且分别满足和，能终止，且分别满足和的状态，那它当然也能终止，且满足的状态，那它当然也能终止，且满足的状态，反之亦的状态，反之亦然然。 3、单调律：如果Q R，则wp(“S”,Q) wp(“S”,R) 4、折取分配律：wp (“S”,Q) wp (“S”,R) wp (“S”, Q R) n确定程序

40、：从某一个状态出发，程序不管执行多少次，所经过的路径相同，所得的结果也相同。wp (“S”,Q) wp (“S”,R)=wp (“S”, Q R) n不确定程序：从某一个状态出发，程序的任何两次执行可能得到的结果都不同，有时即便所得的结果相同，可能经过的路径也不同。wp (“S”,Q) wp (“S”,R) wp (“S”, Q R) 例：抛硬币具有不确定性 wp(“抛硬币”，正面)=F wp(“抛硬币”，反面)=Fwp(“抛硬币”，正面 反面)=T （三）求解最弱前置谓词的规则（三）求解最弱前置谓词的规则 1、skip、abort、复合语句wp(“skip”,R)=R (相当于空语句)wp(

41、“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。B1 cand B2 表示从左到右的

42、次序计算，B1为F时，则不必计算B2,其结果全为F。B1为T时，则其结果为B2的结果。B1无定义时，其结果也无定义。IERIER1.wp(“x:=x+1”,x0)=(x+10)=x-12.wp(“x:=5”,x=5)=5=5=T 3.wp(“x:=5”,x5)=55=F 4.wp(“x:=AB”,P(x)=(B0) cand P(AB) 5.wp(“x:=x *x”, x4=10) =(x*x)4=10)=x8=106.设数组B的下标域为0：100，则: wp(“x:=BI”,x=BI)=(0=I=100) cand BI=BI =0=I0s=(j:0=j0s+bi= (j:0=j=0 s=

43、(j:0=ji:bj)10.Ta:=a+1;b:=xa=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)(3)单个数组元素的赋值语句单个数组元素的赋值语句对一个数组元素的赋值语句 S:=bi:=E其中b是数组名，i是b的下标表达式我们用（b;i:E)表示一个数组函数，定义为： (b; i: E)j= E 当 i=j bj 当ij这样，语句bi:=E等价于b:=(b;i:E)若略去domain(E)与domain(i)等因素，数组的赋值语句语义是wp(“bi:=E”,R)=Rb(b;i: