04 程序正确性证明与分析

第三章 程序的正确性证明一、 F loyd-Hoare 规则公理方法前提条件，初始状态 前置断言结论，终止状态满足的条件 后置断言 程序规范：程序的前置断言和程序的后置断言组成。

程序的状态：程序执行到某一时刻，程序中所有变量的一组取值。

初始状态：所有变量的取值使程序的前置断言为真的状态。

终止状态：所有变量的取值使程序的后置断言为真的状态。

程序的执行可以看作是程序状态的变迁。

1、完全正确性断言：程序S 的执行开始于满足P 的状态，则该执行必定能在有限的时间内终止，且终止的状态满足Q ，则称完全正确性断言，记为{P}S{Q}2、部分正确性断言：程序S 的执行开始与满足P 的状态，若此执行能在有限的时间内终止，则终止时的状态满足Q ，则称部分正确性断言，记为[P]S[Q]（一）预备规则1）如果执行之前P 是真，执行之后Q 也是真，则记为Q P ⊃2) 若n 条路径在语句T 之前汇合，则所有前面语句S i 的结论Q i 都必须在逻辑上蕴含语句T 的前提P ，就是说 P Q i ⊃，其中， i=1,2,…,n.。

P Q ⊃1，P Q ⊃2，P Q ⊃33)若断言P 在条件B 的判断之前成立，则判断的两个结论分别是B P ∧ 和 B P ⌝∧程序，语句 逻辑谓词 逻辑谓词 n2 (0<X<10)P B ⌝4) 若断言P 位于赋值E 于变量I 之后，则P 中出现的所有I 替换成E ，可得到赋值的前提（称赋值等效）。

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

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

','Q Q P P ⊃⊃{P ’}S{Q ’}为真，则{P}S{Q}为真。

（二）Hoare 验证系统 1. 空语句skip {P}skip{P} 结论即为前提2. 赋值语句{IE P } I:=E {P}由规则43. 条件语句{P} if B then S 1 else S 2 {Q} 由规则3得到{B P ∧}S 1{Q}和{B P ⌝∧}S 2{Q}为表示方便，我们可用证明规则的一般形式HH H H n,...,,21来记，其中n H H H ,...,,21是规则的前提，H 是结论，它表示如果’n H H H ,...,,21为真，那么H 也为真。

谈程序的正确性不管在学术圈还是在工业界，总有很多人过度的关心所谓“程序的正确性”，有些甚至到了战战兢兢，舍本逐末的地步。

下面举几个例子：•很多人把测试（test）看得过于重要。

代码八字还没一撇呢，就吵着要怎么怎么严格的测试，防止“将来”有人把代码改错了。

这些人到后来往往被测试捆住了手脚，寸步难行。

不但代码bug百出，连测试里面也很多bug。

•有些人对于“使用什么语言”这个问题过度的在乎，仿佛只有用最新最酷，功能最多的语言，他们才能完成一些很基本的任务。

这种人一次又一次的视一些新语言为“灵丹妙药”，然后一次又一次的幻灭，最后他们什么有用的代码也没写出来。

•有些人过度的重视所谓“类型安全”（type safety），经常抱怨手头的语言缺少一些炫酷的类型系统功能，甚至因此说没法写代码了！他们没有看到，即使缺少一些由编译器静态保障的类型安全，代码其实一点问题都没有，而且也许更加简单。

•有些人走上极端，认为所有的代码都必须使用所谓“形式化方法”（formal methods），用机器定理证明的方式来确保它100%的没有错误。

这种人对于证明玩具大小的代码乐此不疲，结果一辈子也没写出过能解决实际问题的代码。

100%可靠的代码，这是多么完美的理想！可是到最后你发现，天天念叨着要“正确性”，“可靠性”的人，几乎总是眼高手低，说的比做的多。

自己没写出什么解决实际问题的代码，倒是很喜欢对别人的“代码质量”评头论足。

这些人自己的代码往往复杂不堪，喜欢使用各种看似高深的奇技淫巧，用以保证所谓“正确”。

他们的代码被很多所谓“测试工具”和“类型系统”捆住手脚，却仍然bug百出。

到后来你逐渐发现，对“正确性”的战战兢兢，其实是这些人不解决手头问题的借口。

衡量程序最重要的标准这些人其实不明白一个重要的道理：你得先写出程序，才能开始谈它的正确性。

看一个程序好不好，最重要的标准，是看它能否有效地解决问题，而不是它是否正确。

如果你的程序没有解决问题，或者解决了错误的问题，或者虽然解决问题但却非常难用，那么这程序再怎么正确，再怎么可靠，都不是好的程序。

程序正确性证明的方法与技术第一章：引言在计算机科学领域中，程序正确性一直是一个重要的问题。

一个正确的程序能够按照预期的方式运行，并且产生正确的结果。

然而，由于程序的复杂性和人为错误的存在，程序的正确性往往难以保证。

因此，为了确保程序的正确性，人们提出了各种不同的方法和技术来进行程序正确性证明。

第二章：静态分析静态分析是一种常用的程序正确性证明方法。

它通过检查程序的源代码或中间表示来发现潜在的错误。

静态分析可以帮助检测常见的编程错误，如空指针引用、数组越界访问和未初始化变量等。

静态分析工具可以在编译时或者运行时进行分析，并提供相应的警告或错误信息。

静态分析方法有很多种，包括类型检查、数据流分析和符号执行等。

类型检查可以检查程序中变量的类型是否匹配，从而避免类型错误的发生。

数据流分析可以分析程序中数据的流动情况，帮助发现潜在的错误和不一致性。

符号执行是一种通过对程序的符号进行替换和计算来进行分析的方法，它可以发现程序中的不变量和约束条件，并用于证明程序的正确性。

第三章：模型检测模型检测是一种通过构建系统的形式化模型来验证程序的正确性的方法。

它将系统的行为抽象成一组状态和转换规则，并使用逻辑表达式来描述系统的性质。

然后，模型检测工具可以自动地遍历系统的状态空间，并检查所描述的性质是否成立。

模型检测方法可以用于验证各种类型的系统，包括并发系统、分布式系统和硬件系统等。

它可以帮助发现系统中的死锁、活锁和资源竞争等问题，并提供相应的修复建议。

模型检测方法的优势在于它可以自动化地进行验证，并且可以发现系统中的隐藏错误，从而提高程序的可靠性。

第四章：形式化验证形式化验证是一种使用数学方法来证明程序正确性的方法。

它通过将程序的语义和性质形式化为数学公式，然后使用定理证明或模型检验等技术来验证这些公式的真假。

形式化验证方法可以提供严格的证明，从而确保程序的正确性。

形式化验证方法有很多种，包括定理证明、模型检验和符号模型检验等。

1.试比较程序正确性证明与程序测试
正确性证明是论证程序达到预期目的的一般性陈述，而该论证与程序输入数据的特定值无关，能够代表穷举性测试。

程序测试是指测试者特意挑出一批输入数据，通过运行程序，检查每个输入数据所对应的运行结果是否符合预期要求。

Dijkstra说过“程序测试只能证明程序有错，不能说明程序正确”。

除非进行穷举行测试。

2.什么是程序的正确性？试叙述程序正确性证明的基本思想和过程
正确性证明是论证程序达到预期目的的一般性陈述，而该论证与程序输入数据的特定值无关，能够代表穷举性测试。

主要是利用谓词演算和演算规则集合来证明程序的部分正确性。

主要方法。

4.说明程序正确性断言{P}S{Q}的含义，及证明它成立的方法
如何确认一个子类是真正的、忠实的合乎规则的子类型？即子类的类型和父类的类型保持一致所要做的工作是：
从类不变式、方法的前置和后置条件、状态空间和行为等方面加以约束。

第十四讲形式化方法--程序的正确性验证一、概述计算机的程序是一种静态的对象，但它所描述的问题（问题的解）却是一个动态的对象。

所谓的程序设计就是用程序设计语言中的语句改变程序中数据对象的状态，构造所描述问题的动态行为。

这是不自然的，程序所描述的动态行为也无法直接用程序本身的静态结构进行正确性证明。

形式化规约（formal specification）是需求阶段的形式化说明，是用户需求的严格描述，其一般形式用Hoare逻辑描述[1]如下：├{Φ}P{Ψ} <1>其中Φ和Ψ分别表示初始和结束断言条件，其含义是：“假如初始状态d I满足条件Φ，那么程序结束并且终结状态d f必须满足Ψ”。

设D＝D1×……×D n为程序P的状态空间，其中，D j(j=1,……,n)表示程序中数据对象的值域。

显然，由Φ和Ψ断言条件所确定的合法初始和结束状态的集合是D的一个子集。

执行函数E：Φ×P→Ψ定义如下：无定义对合法的初始状态d i，程序P不结束E（P,d I）=终结状态d f对合法的初始状态d i，程序P结束程序的正确性即为：├{Φ}P{Ψ}iff <2>∀d i(├Φ(d i)→(├程序P结束 and ├Ψ(E(P,d i))))总地来讲，验证一个程序的正确与否有两种办法，一种是程序的测试，另一种是程序的正确性证明。

1．程序的测试与程序的验证对给定的一个合法的初始状态d i，当程序执行结束时其终结状态为d f，那么，Φ(d i)和Ψ(d f)都应该被满足。

这一点可用下式表示：{d i}P{d f} <3>所谓程序的测试就是验证测试用例{d i}P{d f}，即验证程序对d i的执行结果是否为d f。

由于合理的初始状态是无限的，因此，对程序验证来讲，测试不是一个完备的方法。

测试被认为是一种尽量发现错误，但并不能保证程序中没有错误[2]的方法。

对大数应用来讲，它是可满足的；但对有些应用来讲，测试是一种不能满足的验证方法，例如：航空、航天等领域的软件系统。