Floyd 1967：归纳断言怎样把程序的意义写在流程图的边上

破除误解：边上的意义不是操作手册，归纳断言也不是终止证明#

第一层误解把「给程序指定意义」听成「写出机器逐步改存储的说明书」，或听成某台编译器的内部表示。弗洛伊德要的是相反的合同：一种程序语言的语义定义，应当独立于该语言的一切处理器。办法是先有语法，再规定哪些短语是命令，再给每类命令一条验证条件，用来约束命令邻域里的标签。满足验证条件的解释，才被承认为合法意义。两个处理器只要都尊重同一套验证条件，已验证的输入输出关系就对两者同时成立。把意义听成「这台机器实际上怎么跑」，会把一次与处理器脱钩的语义提案收成实现注释。

第二层误解把本页收成霍尔三元组的草稿，或收成「弗洛伊德发明了程序证明、霍尔只是换了记号」。霍尔 1969 年点名弗洛伊德。他做的几何不同。本页的基本对象是有向图：顶点上放命令，边上放控制通道，命题贴在连接上。霍尔的基本对象是语言构造：断言夹住一段程序文本。弗洛伊德的赋值验证条件用最强可验证后件来写，方向是从入口标签推出出口标签应满足的蕴涵；霍尔的赋值公理对着后条件往回代入。把 1967 年读成 1969 年的流程图版，会把一次图上的归纳收成一次语法制导公理化的别称。两者可以模拟同一份证明，封面不是同一张图。

第三层误解把边上的命题听成「程序一定会走到出口，并且出口标签为真」。验证条件写明：控制必须离开时，所选出口的标签为真；它不声称控制会离开。弗洛伊德把这种输入输出关系写成：若初始值满足关系 $R_1$，则完成时的终值满足关系 $R_2$。完成是前提。终止要另证，方法是在边上再挂一个取值于良序集的 $W$ 函数，并证明每执行一条命令，出口上的 $W$ 值严格小于入口上的 $W$ 值。良序集里没有无穷下降链，所以全局的停机被收成局部的下降。把归纳断言听成已经证明循环会停，会把后文的良序装置提前写进验证条件。

第四层误解把对象听成循环不变式菜谱，或听成已经交付的自动验证器，或听成诺尔快照的正式版。弗洛伊德写明：正确性与终止的证明方式本身并不新颖，想法来自艾伦·佩利斯（Alan Perlis）与索尔·戈恩（Saul Gorn），最早可能出现在戈恩一篇未发表的论文里。他认为新颖的是：给允许赋值与转移控制的语言建立证明的形式标准，并提议用这套标准来定义语义。自动把未标记的边用最强后件填满，只是文中的可能性，不是本页交付的工具。诺尔的快照没有这套边上的验证条件演算。本页也不把最弱前置条件写成封面。

流程图、验证条件、最强后件与良序下降#

装置从流程图开始，不从 while 语法开始。流程图被松散地定义为有向图：每个顶点放一条命令，边表示命令之间可能的控制通道。指向顶点的边是该命令的入口，离开顶点的边是出口。解释 $I$ 把每条边映到一句命题。命题的自由变元不必全部都是程序变量。对有 $k$ 个入口、$l$ 个出口的命令 $c$，入口标签记作 $P_1,\ldots,P_k$，出口标签记作 $Q_1,\ldots,Q_l$。一份解释的验证，是证明对每条命令：若控制带着为真的 $P_i$ 进入，则它若离开，必带着为真的 $Q_j$ 离开。一类命令的语义定义，就是一条构造验证条件 $V_c(P;Q)$ 的规则：只要每个命令的验证条件被证明，整张图的解释就被验证。

语义定义必须一致：不存在一组自由变元的取值，使入口标签为真而出口标签为假。它最好还完备：任何不满足验证条件的解释都有反例。弗洛伊德写明完备性并非总能得到。底层还有一个演绎系统 $D$，包含带等词的一阶谓词演算的公理与规则。验证条件里的 $\vdash$ 是相对于 $D$ 的可推演。一致性与完备性因此是相对 $D$ 的：赋值算子的语义定义被证明在 $D$ 一致（完备）时自身一致（完备）。

四条一般公理约束任何合格的语义定义。若 $V_c(P;Q)$ 与 $V_c(P';Q')$ 都成立，则合取、析取、对外面那个变元做存在量化之后仍然成立。第四条：前件可加强、后件可减弱。合取用来把分别证明的性质贴到同一条边上。析取用来合并分情形。存在量化说的是：若知道 $x$ 具有性质 $P$ 能保证离开时具有 $Q$，则「存在一个具有 $P$ 的值」也能保证离开时「存在一个具有 $Q$ 的值」。第四条的方向与后来霍尔的推论规则相同，地位不同：它约束的是什么样的 $V_c$ 才算语义定义，不是证明系统里沿语法树走的那条推导规则。不要把公理 4 焊成 1969 年的推论规则。

五种流程图命令给出具体的 $V_c$。赋值 $x \leftarrow f(x,y)$ 的最强可验证后件是 $(\exists x_0)(x = f(x_0,y) \land R(x_0,y))$，其中 $R$ 是入口标签。验证条件说：若这个最强后件能在 $D$ 里推出出口标签 $Q$，则赋值被验证。存在量词是必要的：它记住赋值前的旧 $x$。把赋值听成「执行后 $x$ 等于 $f$，于是把后条件里的 $x$ 换成 $f$」，会在 $f$ 含 $x$ 时立刻写错。分支命令把入口标签与测试 $\phi$ 合取后分别推向真假两路出口。汇合命令要求两路入口标签的析取推出唯一出口标签。起始与停机的验证条件恒真：起始没有入口约束要维护，停机没有出口要交出。图 1 用这些条件验证一个求和流程图：入口 $n$ 为正整数，循环边上保持 $i$ 为整数且 $S$ 等于前 $i-1$ 项之和；若程序终止，完成时 $S$ 为所求的和。验证用到实数、求和与整数的公理，对象仍是边上的标签，不是一份「请按下列步骤发明不变式」的手续。

标签不必事先写满。若入口已标记，且不存在所有边都未标记的闭回路，就可以把某条出口上的标签换成最强后件 $T_c(P)$，而不损失可验证性。$T_c$ 对合取、析取与存在量化分配。弗洛伊德由此写出前面那句自动验证的可能性。本页复述这句话，是为了标明最强后件在原文里的地位，不是为了列出求解器输入格式。

同一套观念被应用到 ALGOL 风格的片段：给语句标前件与后件，再按语句种类写 $V_c$。赋值仍用带存在量词的最强后件，并假定表达式无副作用。条件语句看等价流程图。goto 的顺序出口永不走，对应的验证条件恒真。for、复合、空语句与分程序都有草图。弗洛伊德自己说，对 ALGOL 分程序结构这是糟糕的近似；过程语句的换名参数、动态 own、递归与副作用则不详细处理。封面仍是流程图几何。他证明：在精确算术下，$a := c + (c := c + 1) + c$ 与另外两段无嵌入赋值的语句有相同的验证条件，因而等价。本页不把这段推导展开成改写手册。

终止装置把良序集 $W$ 上的函数挂到每条边上。执行一条命令之后，出口上的 $W$ 值必须严格小于入口上的 $W$ 值。因为 $W$ 没有无穷下降链，程序迟早停。全局性质再次被收成局部论证。最常见的 $W$ 是正整数；弗洛伊德写明，有时用 $n$ 元组的字典序更方便，有时甚至必要。图 5 用二元组 $(X-Q,\ k)$ 证明非负整数 $X$ 除以正整数 $Y$ 的商余算法会停，边上同时维持 $X = R + QY$。霍尔 1969 年的整除例子走同一道算术题，规则换成了 while；本页的下降量写在边上，不是写在语法构造的推论里。弗洛伊德也划了一条与可计算性接壤但不越界的线：若程序的任务是辨认一个递归可枚举但非递归的集合，例如一台机械证明手续，则不能在不损失根本能力的前提下保证终止。归纳断言回答的是「若停，输出满足什么」；良序回答的是「在这个解释下会停」。两句都不是操作单。

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

它证明了：可以给允许赋值与转移控制的语言写一套与处理器无关的语义，使命令的意义成为入口标签与出口标签之间的验证条件；对命令次数的归纳给出部分正确性；良序集上的局部下降给出终止；同一套标签可以证明程序等价。它给出语义定义的一致与完备（相对 $D$）这一对标准，并证明五种流程图命令在该标准下可定义。它把佩利斯与戈恩的断言想法收成可检查的形式对象，并把麦卡锡已对递归函数语言做过的事，明确推广到带赋值与 goto 的命令式图。边上的标签可当说明书，仍不是测试计划。

它没有把语法制导的希尔伯特风格规则写成封面。ALGOL 片段是把同一观念套到语句上，许多规则仍通过「看等价流程图」来辩护；goto、汇合与边上的 $W$ 函数才是本页的几何。它没有给出过程的详细验证条件，也承认分程序处理是近似。它没有提供寻找标签的算法：人提供入口与割边，机器至多沿最强后件往前推并核验蕴涵。把 1967 年听成「从此正确性可自动判定」，会把证明标准收成判定器。任意程序、任意断言的部分正确性，随着语言稍一通用，就会碰上停机问题的边界。弗洛伊德给的是解释与验证条件，让已想到的命题组织成对图的归纳；系统不代替寻找命题，更不裁定任意实例。

它也没有覆盖测试。测例可以展示某个输入上出口标签失败；失败是对该解释的经验反驳。测试不能填满全称量词。两者不是互相取消的替代品。后来的霍尔逻辑、最弱前置条件、相对完备性与工业验证器，都是邻居。本页只把「意义写在边上」钉在 1967 年。

跨域连接#

• 科学哲学：弗洛伊德把一种程序语言收成可检验的理论：验证条件加上演绎系统 $D$，预言「若入口标签为真且控制离开，则出口标签为真」。证伪针对的是处理器，不是单个测例的口碑。一次实现若在入口标签成立时走出了出口标签为假的边，这份理论作为对该处理器的描述就失败；若那次执行根本未离开，部分正确性则从未对该次运行发言。辅助假设与主规则必须分开写：算术公理属于 $D$，命令的 $V_c$ 属于语言合同，良序下降属于终止的另一张支票。把三者捆成一句「程序已被证明」，一次溢出或一次未停都会被误读成「断言方法无用」。1967 年的内容是可验证解释的闭包，不是实验室里「这段代码看起来对劲」的归纳。
• 证明：一份弗洛伊德验证是对象语言之上的形式对象：有限步，每步是某条命令的 $V_c$ 在 $D$ 中成立。对命令次数的归纳，把局部的出口标签接成全局的「若进入则为真」。必然性相对于 $D$ 与那套语义定义，证书是各顶点上的蕴涵，不是一次碰巧成功的执行轨迹。终止证明另造一棵树：边上的 $W$ 值在良序里严格下降。两棵树都是可检查的有限证据。把边上的标签听成已经在机器上跑过一遍，会把句法对象做成运行记录。
• 逻辑：有效性管的是走法，真理性管的是前提。流程图命令本身不是命题；真假落在边上的标签上。验证条件恰好是：若入口标签真，且命令按该类的 $V_c$ 变换状态，则所选出口的标签真。程序对不对，因此被拆成两笔账：一笔是 $D$ 里的谓词推理，一笔是命令如何改写自由变元。把标签听成对业务世界的三段论，会把「$S$ 是前 $i-1$ 项之和」误当成逻辑保证的事实，而它只是某条边上有待维持的断言。逻辑保证的是从公理到该句的走法，不是变量在机器外的含义。
• 认识论：跑通一组输入，得到的是「这些状态下出口标签曾成立」的特称证据。验证一份解释，得到的是全称条件句：凡满足入口标签且确实离开的执行，离开态都在出口标签里。你知道的是条件正确性，不是「它已经停过」。最强后件给出先验的状态变换知识，前提是实现遵守该 $V_c$；编译器是否遵守，要另证。把「已验证解释」听成「每次运行都会结束在出口标签里」，是把条件句做成了无条件占有。

参考文献#

• Robert W. Floyd, "Assigning Meanings to Programs", in J. T. Schwartz (ed.), Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics vol. 19, American Mathematical Society, Providence, 1967, pp. 19–32. —— 本文对象：流程图边上的解释与标签、验证条件、最强后件、ALGOL 片段草图，以及良序集上的终止。
• 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. —— 语法制导的三元组，用以标明本页的边上断言不是对同一几何的更名。
• 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, Amsterdam, 1963, pp. 33–70. —— 弗洛伊德引用的递归方程式语言定义，对照带赋值与转移控制的流程图语义。
• John McCarthy, "Towards a Mathematical Science of Computation", in Proceedings of IFIP Congress 62, North-Holland, Amsterdam, 1962, pp. 21–28. —— 弗洛伊德第二条麦卡锡文献，标明函数式求值不是本页的命令式图。

延伸阅读#

• 与 霍尔 1969：公理基础 对读：霍尔把断言贴在语法构造上；本页贴在图的边上。不要焊成一篇。
• 与 托尼·霍尔 对读：人物页管快速排序、CSP 与空引用；本页停在 1967 年的边上解释。
• 与 逻辑与计算 对读：命题即类型把证明当成程序；本页把程序当成改写边标签的命令。方向相反。
• 与 形式化方法与程序验证 对读：总览页收工具与工业证据；本页只提供归纳断言作为其中一种判断的原句。
• 与 软件测试 对读：测例是特称反驳或未反驳；边上的解释是条件全称。两者不互相替代。
• 与 λ演算与类型理论 对读：代入在 λ 里消函数，在弗洛伊德的赋值里消旧状态。不要把 $x \leftarrow f$ 读成 β 归约。
• 与 可计算性 对读：证明标准存在，不等于任意解释可判定；递归可枚举但非递归的集合挡住的是无损失的终止保证。