计算机程序设计的公理基础

摘要

本文试图借助最初用于几何研究、后来扩展到数学其他分支的技术，探讨计算机程序设计的逻辑基础。这涉及阐明若干组公理和推理规则，它们可用于证明计算机程序的性质。文中给出了这类公理和规则的例子，并展示了一个简单定理的形式证明。最后，本文论证了继续研究这些主题可能带来重要的理论和实践优势。

关键词和短语：公理化方法、程序设计理论、程序证明、形式语言定义、程序设计语言设计、机器无关程序设计、程序文档

CR 分类：4.0, 4.21, 4.22, 5.20, 5.21, 5.23, 5.24

1. 引言

计算机程序设计是一门精确科学，因为一个程序的所有性质，以及它在任意给定环境中执行所产生的一切后果，原则上都可以仅从程序文本本身出发，通过纯粹的演绎推理求出。演绎推理涉及把有效的推理规则应用于若干组有效公理。因此，阐明支撑我们关于计算机程序进行推理的公理和推理规则，是可取且有趣的。公理的具体选择在一定程度上取决于程序设计语言的选择。为便于说明，本文限于一种非常简单的语言；它实际上是所有现行面向过程语言的一个子集。

2. 计算机算术

要对一个程序进行有效推理，首要条件是知道它所调用的基本运算的性质，例如整数的加法和乘法。不幸的是，在若干方面，计算机算术并不等同于数学家熟悉的算术，因此在选择合适的公理集合时必须谨慎。例如，表 I 中列出的公理只是与整数有关的一小部分公理。从这组并不完整的公理，可以推出如下简单定理：

其中第二个定理的证明如下：

其中最后一步要求 \(y \le r\)。

公理 A1 到 A9 当然适用于数学中传统的无限整数集。不过，只要限定为非负数，它们也适用于计算机所操纵的有限“整数”集合。这些公理是否成立与集合大小无关；进一步说，在很大程度上，也与发生“溢出”时所采用的处理技术无关。例如：

(1) 严格解释：溢出运算的结果不存在；当发生溢出时，出错的程序永远无法完成其操作。注意，在这种情况下，A1 到 A9 中的等式是严格的，也就是说，等式两边要么同时存在，要么同时不存在。

(2) 固定边界：溢出运算的结果被取为可表示的最大值。

(3) 模算术：溢出运算的结果按所表示整数集合的大小取模计算。

表 II 通过一个极小模型的加法表和乘法表说明了这三种技术；在该模型中，0、1、2、3 是仅有的整数。

值得注意的是，满足公理 A1 到 A9 的不同系统，可以通过从一组互斥的补充公理中选择某一个而被严格地区分开。例如，无限算术满足公理：

而所有有限算术都满足：

其中 “max” 表示可表示的最大整数。类似地，三种溢出处理方式可以通过选择以下关于 max + 1 取值的公理之一来区分，分别对应严格解释、固定边界和模算术：

选定其中一个公理后，就可以用它来推导程序性质；不过，只有当程序运行在满足所选公理的实现上时，这些性质才必然成立。

3. 程序执行

如上所述，本文研究的目的，是为证明程序性质提供逻辑基础。程序最重要的性质之一，是它是否完成其预期功能。一个程序或程序片段的预期功能，可以通过对相关变量在执行之后将取何值作出一般性断言来指定。这些断言通常不会为每个变量指定具体数值，而是指定这些值及其相互关系所具有的某些一般性质。我们使用数理逻辑中的通常记号来表达这些断言，并尽可能采用熟悉的运算符优先级规则来改善可读性。

在许多情况下，一个程序或程序片段的结果是否成立，将取决于该程序开始执行前变量所取的值。这些成功使用所需的初始前置条件，可以用与描述终止后所得结果相同类型的一般断言来指定。为了说明一个前置条件 (P)、一个程序 (Q) 以及对其执行结果的描述 (R) 之间的必要联系，我们引入一种新的记号：

它可以解释为：“如果断言 P 在程序 Q 启动前为真，那么断言 R 将在它完成时为真。”如果没有施加前置条件，我们写作 true {Q} R。^注1

下面给出的处理方式本质上源于 Floyd [8]，但它被应用于文本而不是流程图。

3.1. 赋值公理

赋值无疑是数字计算机程序设计最具特征性的功能，也是最清楚地区分程序设计与数学其他分支的功能之一。因此，支配我们关于赋值进行推理的公理竟然和初等逻辑中的任何公理一样简单，这一点颇令人惊讶。

考虑赋值语句：

其中：

• x 是一个简单变量的标识符；
• f 是程序设计语言中的一个表达式；它没有副作用，但可以包含 x。

现在，任何关于 x 的断言 P(x)，若要在赋值完成后对 x 的值为真，那么在赋值完成前，它也必须已经对表达式 f 的值为真，也就是说，要以 x 的旧值来求 f。因此，如果 P(x) 要在赋值后为真，那么 P(f) 必须在赋值前为真。这个事实可以更形式化地表达为：

D0（赋值公理）：

其中：

• x 是变量标识符；
• f 是一个表达式；
• P_0 是把 P 中所有出现的 x 都替换为 f 得到的结果。

可以注意到，D0 实际上并不是真正的公理，而是一个公理模式，它描述了一组具有共同模式的无穷公理。这个模式完全用句法术语来描述，因此很容易检查某段有限文本是否符合该模式，从而使它有资格作为一个公理，有效地出现在证明的任意一行中。

3.2. 推论规则

除公理之外，一门演绎科学至少还需要一条推理规则，允许从一个或多个已经证明的公理或定理推出新的定理。推理规则采取这样的形式：“如果 |- X 且 |- Y，那么 |- Z”；也就是说，如果形式为 X 和 Y 的断言已经被证明为定理，那么 Z 也就由此被证明为定理。最简单的推理规则例子说：如果程序 Q 的执行保证断言 R 为真，那么它也保证由 R 在逻辑上蕴含的每一个断言为真。另外，如果已知 P 是程序 Q 产生结果 R 的前置条件，那么任何在逻辑上蕴含 P 的其他断言也同样是这样的前置条件。这些规则可以更形式化地表达为：

D1（后果规则）：

• 若 \(\vdash P \{Q\} R\) 且 \(\vdash R \supset S\)，则 \(\vdash P \{Q\} S\)。
• 若 \(\vdash P \{Q\} R\) 且 \(\vdash S \supset P\)，则 \(\vdash S \{Q\} R\)。

3.3. 组合规则

一个程序通常由一系列依次执行的语句组成。语句之间可以用分号或等价符号分隔，以表示过程性组合：(Q_1; Q_2; ...; Q_n)。为避免省略号带来的笨拙，可以一开始只处理两个语句 (Q_1; Q_2)，因为更长的序列可以通过嵌套重构为 (Q_1; (Q_2; (...(Q_{n-1}; Q_n) ...)))。去掉这个嵌套中的括号，可以看作基于 “; 运算符” 结合性的约定，就像在算术表达式 (t_1 + (t_2 + (...(t_{n-1} + t_n) ...))) 中去掉括号一样。

与组合相关的推理规则说：如果程序第一部分的已证结果，正好等同于第二部分产生其预期结果所需的前置条件，那么只要第一部分的前置条件得到满足，整个程序就会产生预期结果。

更形式化地说：

D2（组合规则）：

• 若 \(\vdash P \{Q_1\} R_1\) 且 \(\vdash R_1 \{Q_2\} R\)，则 \(\vdash P \{(Q_1; Q_2)\} R\)。

3.4. 迭代规则

存储程序计算机的基本特征，是能够重复执行程序的某个部分 (S)，直到某个条件 (B) 变为假。表达这种迭代的一种简单方式，是借用 ALGOL 60 的 while 记号：

while B do S

执行这个语句时，计算机首先测试条件 B。如果它为假，则省略 S，循环执行结束。否则，执行 S，然后再次测试 B。这个动作重复进行，直到发现 B 为假。导致迭代推理规则的思路如下。设 P 是一个断言；只要它在 S 启动时为真，它在 S 完成时也总为真。那么显然，在语句 S 的任意多次迭代之后，P 仍将为真，哪怕迭代零次也是如此。此外，当迭代最终终止时，控制条件 B 已知为假。鉴于在 S 启动时可以假定 B 为真，还可以给出一个稍强的公式：

D3（迭代规则）：

• 若 \(\vdash P \land B \{S\} P\)，则 \(\vdash P \{\text{while } B \text{ do } S\} \neg B \land P\)。

3.5. 例子

上面引用的公理足以构造简单程序性质的证明。例如，可以证明一个例程的性质，该例程用于求 x 除以 y 后得到的商 q 和余数 r。假定所有变量的取值范围都是满足表 I 公理的非负整数集合。为简单起见，我们使用逐次减法这一平凡但低效的方法。所提出的程序是：

((r := x; q := 0); while y <= r do (r := r - y; q := 1 + q))

这个程序的一个重要性质是：当它终止时，我们可以通过把余数 r 加上除数 y 与商 q 的乘积来恢复被除数 x，也就是 x = r + y * q。此外，余数小于除数。这些性质可以形式化地表达为：

其中 Q 表示上面展示的程序。这表达了程序“正确性”的一个必要但并不充分的条件。

表 III 给出了这个定理的形式证明。像所有形式证明一样，它过于冗长；引入一些记号约定来显著缩短它并不困难。减少形式证明冗长性的一个更强方法，是从作为公设接受的简单规则中推导出用于构造证明的一般规则。这些一般规则的有效性，可以通过证明每一个借助它们证明出的定理，同样都可以在不借助它们的情况下被证明出来来说明，只是那样会更加冗长。一旦发展出一套强有力的补充规则，“形式证明”就会简化为不过是对一个形式证明如何构造的非形式提示。

4. 一般保留意见

本文引用的公理和推理规则，隐含地假定表达式和条件的求值没有副作用。如果要证明用允许副作用的语言写成的程序性质，就必须在每一种情况下先证明这些副作用不存在，然后才能应用相应的证明技术。如果高级程序设计语言的主要目的，是帮助构造和验证正确的程序，那么用函数式记法调用带副作用的过程是否真有优势，是值得怀疑的。

上面引用的公理和规则还有一个缺陷：它们并没有为证明程序成功终止提供基础。无法终止可能是由于无限循环；也可能是由于违反了由实现定义的某个限制，例如数值操作数的范围、存储大小，或操作系统时间限制。因此，记号 “P {Q} R” 应解释为：“假如程序成功终止，那么其结果的性质由 R 描述。”调整这些公理，使它们不能用于预测非终止程序的“结果”，是相当容易的；但公理的实际使用现在就会依赖于许多实现相关特性的知识，例如计算机的大小和速度、数的范围，以及溢出技术的选择。除了证明避免无限循环之外，更好的做法大概是证明程序的“条件”正确性，并依赖某个实现来发出警告，如果它由于违反实现限制而不得不放弃执行该程序的话。

最后，有必要列出一些尚未覆盖的领域：例如实数算术、位和字符操作、复数算术、分数算术、数组、记录、覆盖定义、文件、输入/输出、声明、子例程、参数、递归以及并行执行。即使是对整数算术的刻画也远未完成。只要程序设计语言保持简单，处理这些问题似乎并没有太大困难。真正带来困难的领域是标号和跳转、指针以及名字参数。使用这些特性的程序，其证明很可能会很繁复；这反映在底层公理的复杂性中，也就并不令人意外。

5. 程序正确性证明

程序最重要的性质，是它是否完成了使用者的意图。如果这些意图可以通过对程序执行结束时，或中间点处，变量取值作出断言来严格描述，那么本文所述技术就可以用来证明程序的正确性，前提是程序设计语言的实现符合证明中所用的公理和规则。这个事实本身也可以通过演绎推理来确立，所用的公理集合描述硬件电路的逻辑性质。当一个程序、它的编译器以及计算机硬件的正确性全都以数学确定性确立之后，人们就有可能高度信赖程序结果，并以只受电子器件可靠性限制的信心预测这些结果的性质。

为非平凡程序提供证明的实践，只有到相当更强大的证明技术可用之后才会普及；即便如此，它也不会容易。但是，鉴于程序错误成本不断增加，程序证明的实际优势最终会超过其困难。目前，程序员用来使自己相信程序正确的方法，是在一些特定案例中试运行它，并在产生的结果不符合意图时修改它。在找到足够多样的一组例子、程序在这些例子上看起来都能工作之后，他就相信它将总是工作。花在这种程序测试上的时间，通常超过整个程序设计项目时间的一半；如果对机器时间作现实的成本估算，项目成本的三分之二或更多都用于在这个阶段排除错误。

程序投入使用后才发现的错误，其排除成本往往更高，特别是对计算机制造商的软件项目而言，其中很大一部分费用由用户承担。最后，在某些类型的程序中，错误的代价可能几乎无法估算，比如一艘失事的航天器、一座倒塌的建筑、一架坠毁的飞机，或一场世界大战。因此，程序证明的实践不仅是一种为学术声誉而从事的理论追求，而且是降低与程序错误相关成本的一项严肃建议。

程序证明的实践还可能缓解计算世界中的其他一些问题。例如，程序文档问题就是其中之一。文档之所以必要，首先是为了告知某个子例程的潜在用户如何使用它以及它完成什么；其次是为了在需要更新程序以适应变化的环境，或根据增加的知识改进程序时，辅助进一步开发。对一个子例程的目的以及正确使用条件作出表述，最严格的方法是对其执行前后变量的值作出断言。随后，对这些断言正确性的证明，可以作为任何调用该子例程的程序证明中的引理。因此，在一个大型程序中，整体结构可以清楚地映射到其证明结构中。此外，当必须修改程序时，总可以用另一个满足同一正确性准则的子例程替换任意子例程。最后，在考察算法细节时，证明很可能有助于解释不仅发生了什么，而且解释为什么会发生。

在可解决的范围内，程序证明的实践还可以解决另一个问题，即把程序从一种计算机设计转移到另一种计算机设计。即使程序是用所谓机器无关的程序设计语言编写的，许多大型程序也会无意中利用某个特定实现的某些机器相关性质；当试图把它转移到另一台机器上时，可能出现令人不快且代价高昂的意外。不过，任何机器相关特性的存在，都会通过从机器无关公理出发证明程序的尝试失败而预先暴露出来。于是程序员可以选择以机器无关的方式表述其算法，必要时借助环境查询；或者，如果这需要太多努力或效率太低，他也可以有意构造一个机器相关程序，并在证明中依赖某个机器相关公理，例如 A11 的某个版本（第 2 节）。在后一种情况下，必须把该公理明确列为成功使用该程序的一个前置条件。这个程序仍然可以完全放心地转移到任何恰好满足同一个机器相关公理的其他机器上；但如果必须把它转移到一个不满足该公理的实现上，那么所有需要修改的位置都会由这样一个事实清楚地标注出来：该处证明诉诸了那个有问题的机器相关公理为真。

因此，程序证明的实践似乎会导向软件和程序设计中三个最紧迫问题的解决，即可靠性、文档和兼容性。不过，至少在当前，程序证明即使对高水平程序员来说也很困难；并且可能只适用于相当简单的程序设计。和其他领域一样，可靠性只能以简单性为代价来购买。

6. 形式语言定义

高级程序设计语言，例如 ALGOL、FORTRAN 或 COBOL，通常预期要在大小、配置和设计各不相同的多种计算机上实现。要以足够严格的方式定义这些语言，以确保所有实现者之间的兼容性，已经被证明是一个严重问题。既然兼容性的目的在于便利用该语言表达的程序之间的互换，那么实现这一点的一种方式，是坚持要求该语言的所有实现都“满足”支撑该语言程序性质证明的公理和推理规则，从而使所有基于这些证明的预测都将实现，除非发生硬件故障。实际上，这等同于把这些公理和推理规则接受为该语言意义的最终决定性规约。

除了为实现的正确性给出一个直接的、甚至可能可证明的准则之外，用于定义程序设计语言语义的公理化技术，似乎类似于 ALGOL 60 报告中的形式语法，因为它足够简单，既能被实现者理解，也能被相当成熟的语言用户理解。只有在单个文档中弥合这种不断扩大的沟通鸿沟，也许甚至以可证明一致的方式弥合它，形式语言定义才能获得最大优势。

使用公理化方法的另一大优势，是公理为允许语言的某些方面保持未定义提供了一种简单而灵活的技术，例如整数范围、浮点精度以及溢出技术的选择。这对标准化目的绝对必要，因为否则该语言将不可能在不同硬件设计上高效实现。因此，一个程序设计语言标准应当包含一组普遍适用的公理，同时还要包含一组补充公理中的选择项，用来描述实现者所面对的选择范围。第 2 节给出了为此目的使用公理的一个例子。

形式语言定义的另一个目标，是帮助设计更好的程序设计语言。ALGOL 60 语法的规则性、清晰性和易实现性，至少部分可能归功于使用了一种优雅的形式技术来定义它。公理的使用可能在“语义”领域带来类似优势，因为一种可以由少量“不证自明”的公理描述、并且证明相对容易构造的语言，似乎会优于一种具有许多晦涩公理且难以在证明中应用的语言。此外，公理使语言设计者能够相当简单而直接地表达其总体意图，而不必给出通常伴随算法式描述的大量细节。最后，公理可以以彼此基本独立的方式来表述，使设计者可以自由处理某一个公理或一组公理，而不必担心它们与语言其他部分产生意外的相互作用。

致谢。许多关于计算机程序设计的公理化处理 [1]、[2]、[3] 解决的是证明算法等价性，而不是证明算法正确性的问题。其他方法 [4]、[5] 则以递归函数而不是程序作为理论起点。使用公理来定义计算机原始操作的建议见于 [6]、[7]。程序证明的重要性在 [9] 中得到了明确强调，其中还描述了一种提供程序证明的非形式技术。对证明技术的规约可以为程序设计语言提供充分的形式定义，这一建议最早见于 [8]。本文给出的程序执行形式处理显然源自 Floyd。作者的主要贡献似乎是：(1) 提出公理可以为保留语言某些方面未定义这一问题提供一种简单解决办法；(2) 全面评价采用这种方法对程序证明和形式语言定义两方面可能带来的收益。

不过，本文提出的形式材料只具有说明性质，并且只占仍待完成工作中极小的一部分。希望其中涉及的许多迷人问题将由其他人继续研究。

RECEIVED NOVEMBER, 1968; REVISED MAY, 1969

^注1 如果这可以在我们的形式系统中证明，我们就使用熟悉的定理性逻辑符号：`|- P {Q} R` ↩

References

1. Yanov, Yu I. Logical operator schemes. Kybernetika 1, (1958).
2. Igarashi, S. An axiomatic approach to equivalence problems of algorithms with applications. Ph.D. Thesis 1964. Rep. Compt. Centre, U. Tokyo, 1968, pp. 1-101.
3. de Bakker, J. W. Axiomatics of simple assignment statements. M.R. 94, Mathematisch Centrum, Amsterdam, June 1968.
4. McCarthy, J. Towards a mathematical theory of computation. Proc. IFIP Cong. 1962, North Holland Pub. Co., Amsterdam, 1963.
5. Burstall, R. Proving properties of programs by structural induction. Experimental Programming Reports: No. 17 DMIP, Edinburgh, Feb. 1968.
6. van Wijngaarden, A. Numerical analysis as an independent science. BIT 6 (1966), 66-81.
7. Laski, J. Sets and other types. ALGOL Bull. 27, 1968.
8. Floyd, R. W. Assigning meanings to programs. Proc. Amer. Math. Soc. Symposia in Applied Mathematics, Vol. 19, pp. 19-31.
9. Naur, P. Proof of algorithms by general snapshots. BIT 6 (1966), 310-316.