跳转到内容
← 返回计算理论
计算理论当代约 19 分钟阅读

Hoare 1969：公理基础怎样把程序正确性写成可推导的三元组

An Axiomatic Basis for Computer Programming

Hoare三元组赋值公理推论规则部分正确性CACM 1969

1969 年 10 月，《美国计算机学会通讯》（Communications of the ACM）第 12 卷第 10 期发表 C. A. R. 霍尔（Charles Antony Richard Hoare）的《An Axiomatic Basis for Computer Programming》，页码 576 至 580、583。DOI 为 10.1145/363235.363259。中间空出的两页是当期广告，不是正文缺页。作者当时在贝尔法斯特女王大学。本页的对象是这份已发表的短文：用断言夹住一段程序，把「若执行前 $P$ 真，且该段终止，则执行后 $R$ 真」写成可推导的判断，并给出赋值公理与两条推论规则。原文记号是 P {Q} RP\ \{Q\}\ R，程序写在花括号里；后来通行的 {P} S {Q}\{P\}\ S\ \{Q\} 把断言挪到两侧，判断相同，排版不同。本页两套都认，推导按原文的 $D0$ 到 $D4$ 走。

它不是 托尼·霍尔 的人物页。快速排序、空引用与 1978 年的通信顺序进程都不在这五页里。它不是 逻辑与计算 的总览：柯里–霍华德把证明当成函数式项，本页把命令当成对状态断言的改写。它不是 形式化方法与程序验证 的工具地图，没有模型检验、定理证明器名单或工业案例。它不是验证操作单，不教怎样选循环不变式去喂求解器。它也不是 软件测试 的事故史，不是 λ演算与类型理论 的命题即类型，不是 可计算性 的停机判定，更不是 计算机体系结构 的指令集手册。机器整数的溢出只作为公理该弱到哪一步出现。

破除误解：三元组不是终止证明，赋值也不是往前代换

第一层误解把 P {Q} RP\ \{Q\}\ R 听成「程序一定会停，并且停在 $R$」。霍尔写明：该判断不声称 $Q$ 终止。若 $Q$ 从满足 $P$ 的状态出发永不结束，就不存在「完成时 $R$ 失败」的反例，判断仍可成立。这是后来所称的部分正确性。全正确性还要另给一个随循环严格下降的量，1969 年的编号规则里没有这一条。把三元组听成「已经证明它会停」，会把后年的变式论证提前写进这一期。

第二层误解把赋值听成往前代换：执行 $x := f$ 之后，$x$ 等于 $f$，于是把后条件里的 $x$ 换成 $f$ 就算证完。这在 $f$ 含 $x$ 时立刻崩掉。$x := x+1$ 之后并没有 $x = x+1$。公理的方向相反。若执行后要 $P$，执行前必须已经有把 $P$ 里自由的 $x$ 全部换成 $f$ 所得的 P0P_0。记号是 ⊢P0 {x:=f} P\vdash P_0\ \{x := f\}\ P。想要 {x=n}\{x = n\} 在 $x := x+1$ 之后成立，事前需要 $x+1 = n$，也就是 $x = n-1$。推理对着后条件往回走。把赋值写成「往前代换」，会在自增、累加这类最普通的语句上造出矛盾式。

第三层误解把这份短文收成流程图上的断言法，或收成「霍尔发明了程序证明」。罗伯特·弗洛伊德（Robert W. Floyd）1967 年在美国数学会应用数学讨论会上发表《Assigning Meanings to Programs》，对象见 Floyd 1967，把断言写在流程图的边上，用归纳断言说明每条边被穿过时成立。彼得·诺尔（Peter Naur）1966 年在 BIT 上用「一般快照」写下算法中途必须为真的画面。约翰·麦卡锡（John McCarthy）更早用递归方程给语言写数学定义。霍尔在文中点名这些人。他做的几何不同：断言贴在语言构造上，而不是贴在图画的边上。顺序、循环各有一条规则，证明随语法树组合。把 1969 年读成对弗洛伊德的更名，会把一次语法制导的公理化收成一张流程图的别称。

第四层误解把对象听成验证菜谱，或听成后来教材默认的 {P} S {Q}\{P\}\ S\ \{Q\} 加上分支规则、过程规则、分离逻辑的全套。原文编号到迭代为止：赋值、推论、复合、循环。分支、过程、指针别名、并发都不在 $D0$–$D4$ 里。推论规则说的是断言之间的蕴涵，不是「把程序改得更好」。本页也不把最弱前置条件演算写成封面：那是戴克斯特拉稍后的整理。把工具链、求解器与循环不变式写法读回这五页，会把一条证明系统收成操作手册。

机器整数、赋值公理、推论与复合

装置从整数开始，不从语法糖开始。霍尔要求：算术公理必须对数学整数与机器上能表示的有限整数同时成立。交换律、结合律一类共享性质可以写进公理；「任意大的后继仍是整数」不能写进去，因为字长会把它证伪。溢出被留作实现的自由：可以拒绝完成这次运算，也可以让结果在公理之外未定义。用共享公理推出的三元组，在「运算若完成、则满足这些等式」的前提下，对两类整数都有效。这不是把机器算术等同于皮亚诺算术，而是把证明故意停在两者尚未分叉的那一层。字长、补码与溢出陷阱属于机器合同；本页只要这句分层。

程序执行被收成对断言的变换。P {Q} RP\ \{Q\}\ R 读作：若启动 $Q$ 前 $P$ 为真，则 $Q$ 完成时 $R$ 为真。$P$、$R$ 是关于程序变量的逻辑断言，不是输出日志，也不是测试向量。语言在本页里被当成待公理化的对象：先规定哪些三元组可从公理推出，再把推出关系当作该语言的一种定义。这与「先写一台抽象机、再看它逐步改存储」的操作语义不是同一份合同。霍尔把它当作语言定义的候选方法之一，并不声称已经取代实现者手里的那台机器。

赋值公理是唯一的公理图式。设 P0P_0 由 $P$ 把自由出现的 $x$ 全部换成 $f$ 得到，则 ⊢P0 {x:=f} P\vdash P_0\ \{x := f\}\ P。代入必须避开被绑定量词抓住的同名变元，文中按一阶逻辑的通常谨慎处理。这条公理假设 $x$ 是一个简单变量，$f$ 的求值没有副作用，并且没有另一个名字指向同一位置。若 $x$ 与 $y$ 是同一单元的两个名字，则 $x := 1$ 不能保证 $y$ 仍是旧值，公理失效。1969 年把失效写进后文的保留意见，并不在当时修补。别名、指针与堆上的分离，是后年的另一些逻辑，不是本页的规则表。

两条推论规则把断言的强弱从程序上揭下来。若已有 ⊢P {Q} R\vdash P\ \{Q\}\ R 且 ⊢R⊃S\vdash R \supset S，则 ⊢P {Q} S\vdash P\ \{Q\}\ S：后条件可以减弱。若已有 ⊢P {Q} R\vdash P\ \{Q\}\ R 且 ⊢S⊃P\vdash S \supset P，则 ⊢S {Q} R\vdash S\ \{Q\}\ R：前条件可以加强。方向不可反。从 {x>2} S {y=0}\{x>2\}\ S\ \{y=0\} 推不出 {x>1} S {y=0}\{x>1\}\ S\ \{y=0\}，因为更弱的前条件包含公理尚未覆盖的状态。从 {x>2} S {y=0}\{x>2\}\ S\ \{y=0\} 也推不出 {x>2} S {y=0∧z=1}\{x>2\}\ S\ \{y=0 \wedge z=1\}，因为更强的后条件多要了程序未必维护的事实。推论规则所消耗的 ⊃\supset，是断言语言里的定理，不是程序文本里的新命令。霍尔把「证明一段算术事实」与「证明一段命令变换断言」分成两层，正是为了让后一层保持短。

复合规则把顺序接起来。若 ⊢P {Q1} R1\vdash P\ \{Q_1\}\ R_1 且 ⊢R1 {Q2} R\vdash R_1\ \{Q_2\}\ R，则 ⊢P {Q1;Q2} R\vdash P\ \{Q_1; Q_2\}\ R。中间断言 R1R_1 必须写出来，它不是机器自动填的空。迭代规则处理 while B do S。若 ⊢P∧B {S} P\vdash P \wedge B\ \{S\}\ P，则 ⊢P {while B do S} P∧¬B\vdash P\ \{\texttt{while } B \texttt{ do } S\}\ P \wedge \neg B。$P$ 在循环体下被保存，离开时再合上条件的否定。$P$ 后来叫循环不变式。规则并不告诉你 $P$ 是哪一句：它只说，若你已经为体证明了「$P$ 且 $B$ 推出体之后仍是 $P$」，整个循环就交出 $P$ 且非 $B$。寻找那句 $P$，不是 1969 年给出的算法。把规则听成「请按下列步骤发明不变式」，会把存在性的推导规则收成合成手续。

文中的例子是整除。给定 $y>0$，执行 r:=x; q:=0;r := x;\ q := 0; 再 while y ≤ r do (r := r − y; q := q + 1)。要证完成时 x=r+y×qx = r + y \times q 且 $r < y$。不变式取 x=r+y×qx = r + y \times q。两次赋值之后它立刻成立。循环体里先减 $r$ 再加 $q$，用赋值公理从后往前代换：要在 $q := q+1$ 之后维持该式，事前需要 x=r+y×(q+1)x = r + y\times(q+1)；再对 $r := r-y$ 代换，事前回到 x=r+y×qx = r + y\times q。体的前条件还带着 y≤ry \le r，离开循环时得到 $r < y$。全程没有证明循环会停：若 y≤0y\le 0，这台纸上的机器可以永不退出。部分正确性在这里是精确的，不是谦虚的修辞。本页复述这条推导，是为了标明 $D0$ 与 $D4$ 在原文里怎样合用一次，不是为了列出「除法程序验证步骤」。霍尔还写了一句常被收成工程口号的用途：同一套三元组可以用来说明两段程序在断言层面等价，因而把较慢的写法换成较快的写法时，不必重新发明后条件。等价在这里仍是部分正确性上的等价，不是时钟周期上的保证。本页不把那句话展开成改写手册。

它证明了什么，没有覆盖什么

它证明了：可以给命令式小语言写一套希尔伯特风格的公理与规则，使程序正确性成为相对断言语言的形式推导；赋值的代入方向必须向后；推论允许加强前条件、减弱后条件；顺序靠中间断言衔接；循环靠不变式把潜在无限次体执行收成一次保存性。它给出一种语言定义策略：语义是「哪些三元组可证」，而不是「抽象机如何改写存储」。满足同一套公理的两种实现，应让已推出的三元组一同成立：证明跟着合同走，不跟着某台编译器的内部表示走。机器整数被处理成与数学整数共享一组较弱公理的对象，从而使同一份证明在溢出被当成未完成或未定义时仍然可读。文档功能被他写成副产物：中间断言就是程序在断言语言里的说明书，而不是另贴的注释。副产物仍不是测试计划。

它没有证明终止。迭代规则的结论可以在永真的循环上成立。它没有给出分支、过程、换名参数、goto、表达式副作用或并行的编号规则。文末「一般保留」把这些列为当时尚未收进公理的裂缝。别名使赋值公理失效，这一句已经足够把后来堆逻辑的动机标成邻居，而不把邻居写进封面。它也没有给出相对于一阶算术的完备性：斯蒂芬·库克 1978 年才把相对完备性写成定理。1969 年提供的是一套被认为合理的规则，不是「凡真三元组皆可在该系统内推出」的元定理。

它没有提供判定手续。任意程序、任意断言的部分正确性，随着语言稍一通用，就会碰上停机问题的边界：不存在能对所有输入都停机并答对的算法，去裁定任意三元组是否为真。霍尔给的是证明系统，让人把已想到的断言组织成推导；系统不代替寻找断言，更不决定任意实例。把公理基础听成「从此正确性可自动判定」，会把形式系统收成判定器。测试仍然可以展示某个输入上 $R$ 失败；失败是对三元组的经验反驳。测试不能填满全称量词。两者在本页里不是互相取消的替代品，而是不同的证据种类。戴克斯特拉 1968 年在 BIT 上的构造性正确性讨论是文中引用的邻居，不是本页的规则表。

稳健性来自语法组合，不来自后来的产品。只要赋值仍是对简单变量的无副作用写入，代入公理就仍是局部的。语言一旦加入别名、异常或并发写入，局部性先碎，规则必须重写，而不是把 1969 年的 $D0$ 硬套上去。弗洛伊德的边上断言可以模拟同一份证明，几何不同：图的归纳对任意跳转更顺，语法制导对结构化命令更顺。两种几何在 1960 年代末并行，不是一次命名权争夺。公理语义作为语言定义，后来与操作语义、指称语义并列；本页只把「用可证三元组当定义」这一提案钉在 1969 年，不写斯科特与斯特雷奇的后话。概念证据到此为止。三元组回答的是「正确性在这一年用哪一种判断写下」；代入方向回答的是「赋值怎样改断言」。两句都不是操作单。

跨域连接

  • 科学哲学：霍尔把一种程序语言收成可检验的理论：共享算术公理加上 $D0$–$D4$，预言「若运算完成且证明给出 $R$，完成态应满足 $R$」。证伪针对的是实现，不是单个测例的口碑。一次溢出若被当成普通结果、又破坏了共享等式，这份理论作为对该机器的描述就失败；若溢出被规定为未完成，理论则从未对该次执行发言。辅助假设与主规则必须分开写，否则一次字长事故会被误读成「公理方法无用」。1969 年的内容是可证闭包，不是实验室里「这段代码看起来对劲」的归纳。把科学理论听成对单个谜题的直觉，会把一次公理提案收成编程经验谈。
  • 逻辑：有效性管的是走法，真理性管的是前提。霍尔三元组是关于命令的判断，命令本身不是命题；真假落在两侧的断言上。推论规则恰好是：若已有三元组，且断言之间的蕴涵有效，则可改写两侧。程序对不对，因此被拆成两笔账：一笔是断言语言里的谓词推理，一笔是命令如何改写自由变元。把三元组听成对业务世界的三段论，会把「$x$ 是余数」误当成逻辑保证的事实，而它只是后条件里的一句有待维持的断言。逻辑保证的是从公理到该句的走法，不是变量在机器外的含义。
  • 认识论：跑通一组输入，得到的是「这些状态下 $R$ 曾成立」的特称证据。推出 P {Q} RP\ \{Q\}\ R，得到的是全称条件句：凡满足 $P$ 且确实完成的执行，完成态都在 $R$ 里。知识的模态被写进判断里：你知道的是条件正确性，不是「它已经停过」。终止仍是未证明的经验或另证。赋值公理给出的是先验的状态变换知识，前提是语言实现遵守该公理；编译器是否遵守，要另用对实现的知识来担保。把「我已经证明三元组」听成「我已经知道每次运行都会结束在 $R$」，是把部分正确性的条件句做成了无条件占有。
  • 公理：公理在这里不是「显然为真的机器事实」，而是为这场推理游戏选定的初始规则。霍尔刻意选用对有限字长与无限整数都成立的较弱算术，等于承认换一套字长合同就会换一座大厦。溢出被留作可选择的附加规则，很像平行公设：不写进共享核心，以免把一种实现的偶然性做成全部实现的必然性。一致性的压力立刻可见：赋值公理与别名不能共存于同一套不改写的规则。独立性也可见：推论规则推不出赋值的代入方向，必须单列。把公理听成对 1969 年某台机器的实测报告，会把形式系统收成硬件说明书。
  • 证明：一份霍尔推导是对象语言之上的形式对象：有限步，每步是 $D0$ 或一条规则。它不是欧几里得式的「对所有几何图形必然」，而是「在该语言的公理下，从 $P$ 可推出完成时的 $R$」。必然性相对于公理，证书是那棵推导树。树的叶子上往往还挂着断言语言里的算术引理，那些引理的证明属于另一套系统。把三元组的推导听成已经在机器上跑过一遍，会把句法对象做成运行记录。1969 年要的是可检查的有限证据，不是一次碰巧成功的执行轨迹。

参考文献

  • C. A. R. Hoare, "An Axiomatic Basis for Computer Programming", Communications of the ACM 12(10), 1969, pp. 576–580, 583. DOI: 10.1145/363235.363259. —— 本文对象：三元组判断、赋值公理、推论与复合、迭代，以及机器算术的共享公理。
  • Robert W. Floyd, "Assigning Meanings to Programs", in Proceedings of Symposia in Applied Mathematics, Vol. 19, American Mathematical Society, 1967, pp. 19–32. —— 流程图边上的归纳断言，用以标明本页的语法制导不是对同一几何的更名。
  • Peter Naur, "Proof of Algorithms by General Snapshots", BIT 6(4), 1966, pp. 310–316. —— 中途快照，用以标明 1960 年代中期并行的断言想法。
  • John McCarthy, "A Basis for a Mathematical Theory of Computation", in P. Braffort & D. Hirschberg (eds.), Computer Programming and Formal Systems, North-Holland, 1963, pp. 33–70. —— 文中引用的递归方程式语言定义，对照公理定义。
  • Edsger W. Dijkstra, "A Constructive Approach to the Problem of Program Correctness", BIT 8(3), 1968, pp. 174–186. —— 文中引用的正确性讨论，用以标明最弱前置条件不是 1969 年的封面。
  • A. van Wijngaarden, "Numerical Analysis as an Independent Science", BIT 6(1), 1966, pp. 66–81. —— 数值分析与机器算术的分家，呼应本页把共享公理与溢出分开写。

延伸阅读

  • 与 托尼·霍尔 对读：人物页管快速排序、CSP 与空引用；本页停在 1969 年的 $D0$–$D4$。
  • 与 逻辑与计算 对读：命题即类型把证明当成程序；本页把程序当成改写断言的命令。方向相反。
  • 与 形式化方法与程序验证 对读：总览页收工具与工业证据；本页只提供三元组作为其中一种判断的原句。
  • 与 软件测试 对读：测例是特称反驳或未反驳；三元组是条件全称。两者不互相替代。
  • 与 λ演算与类型理论 对读：代入在 λ 里消函数，在霍尔里消状态变元。不要把 $x := f$ 读成 β 归约。
  • 与 可计算性 对读：证明系统存在，不等于任意三元组可判定。停机边界挡住的是后者。

正文中引用本条 · 4