用标准程序设计语言编写的程序的正确性证明

3.1 引言 在前一章所讨论的归纳断言法,可以直接用来证明用一种标准程序设计语言,比如FORTRAN、ALGOL、或PL/1编写的计算机程序的(部分)正确性。这种程序的终止也可以用前面讲的同一方法来证明。应用归纳断言法证明时。

流程图程序的正确性证明

2.1 引言 当我们编制计算机程序时,我们的目的是程序要实现某种特定的计算。但是,正象许多程序设计者感到伤脑筋的那样,我们所编写的程序大多难免有错误(或故障)。所以,通常要花费很多程序设计时间来测试和排除我们所编写的(不正确的)程序。

与程序正确性证明有关的当前研究动向

5.1 引言 关于程序正确性证明这一领域目前已进行了大量的研究。这里,为了便于讨论,我们把这些研究分成如下几方面: 1.关于证明(部分)正确性和终止的证明技术。 2.有关程序正确性的程序设计和语言设计的一些考虑。

递归程序的正确性证明

4.1 引言 许多程序设计语言(例如,ALGOL、PL/1、LISP)是允许程序员用来编写递归程序的;即作为其计算时调用它自身部分的程序(递归地)恰好与一个非递归程序一样可调用辅程序。这种递归程序在处理具有递归定义数据结构比如表格或树状是非常有用的。这种递归程序是以一种语言比如LISP为基础的。

序

本书的意图是阐明和举例说明计算机程序正确性证明的一些基本技术。近几年来,致力于这一课题的研究已取得了巨大的成果。这些研究的大部分都是针对着证明的形式化和最终的机械化。但是,我们强调的却是这种典型的相当非形式的正确性证明(程序员可用它来设法系统地确定其本身的程序正确性)。当然,我们将会发觉非形式的正确性证明可能容易出错。因而,它并不是予防或者发现一切程序设计错误的灵丹妙药。但是。

A QUANTIFIER-ELIMINATION BASED HEURISTIC FOR AUTOMATICALLY GENERATING INDUCTIVE ASSERTIONS FOR PROGRAMS

用量词消除的一个方法为自动地产生程序 invariants/inductive 断言被建议。给一个程序，引入的断言，在一个理论作为 parameterized 假设了公式，与程序地点被联系。在引入的断言的参数被由保证引入的断言被导致程序的联系地点的所有实行路径确实保存在参数上产生限制发现。方法能被用来发现在一个环的入口仍然保持不变的变量不变性质的循环。parameterized 公式能被一个一个地考虑实行路径连续地精制；启发规则能为决定路径在被考虑的顺序被开发。如果可得到，象前提和帖子一样的变量调节的节目的初始化，能也被用来进一步精制假设不变。方法不取决于一个程序的前提 andpostcondition 的可获得性。这样产生的参数上的限制为参数的可能的价值被解决。如果没有解决方案是可能的，这意味着那一假设形式不变不是可能的在做产生联系确认条件的假设 / 近似下面为循环存在。不同如果参量的限制是可解决的，那么在为产生这些限制的方法上的某些条件下面，最强壮可能假设形式不变能从参量的限制的很一般的答案被产生。途径为表示断言象 Presburger 算术一样用多项式方程的连词的逻辑语言被说明。