Hoare逻辑

CST Part II 课程的学习指南. 本文档旨在提供背景阅读材料以支持讲座——可以将其视为一本免费的可下载教科书. 第1到5章介绍了Floyd和Hoare提出的程序规约与证明的经典思想. 尽管大部分材料已经很老——请看一些被引用参考文献上的日期——它仍然是当前研究的基础. 第6章是对程序精化的一个非常简要的介绍; 它提供了从Hoare风格的规约计算出一个实现的规则. 第7章是对分离逻辑思想的介绍, 分离逻辑是Hoare逻辑的一个扩展, 用于规约和验证操纵指针的程序. 分离逻辑建立在Burstall的早期思想之上, 但其现代形式归功于O'Hearn和Reynolds.

请注意, 讲座中呈现的一些主题可能未在本文档中涵盖, 本文档中的一些材料也可能与讲座中涵盖的主题无关. 例如, 程序精化和分离逻辑的主题可能只会被非常粗略地描述, 如果有涉及的话. 考试题目将基于讲座中呈现的材料.

Part II课程Hoare Logic是从一门更早的Part II课程演变而来的, 该课程的网页可以在我的主页上找到 (www.cl.cam.ac.uk/~mjcg). 那门课程的一些考试题目可能是很好的练习 (但请注意其中一些是基于本课程未涵盖的材料). 一份包含当前课程练习题的单独文档可从网页获取.

警告. 这里的材料由过去课程讲义的重新组织的摘录以及新材料组成. 很有可能存在符号不一致, 遗漏和错误. 如果您发现此类缺陷, 请将详细信息发送至Mike.Gordon@cl.cam.ac.uk.

致谢. 感谢Martin Vechev和John Wickerson在这些笔记的先前草稿中发现了许多错误 (其中一些是严重的), 同时也感谢他们对改进文本提出的建议.

第1章程序规约

本章引入了一种包含赋值, 条件式, 块和

WHILE

循环的简单编程语言. 然后用它来描述Hoare用于规约程序部分正确性的记号. Hoare的记号使用形式逻辑记号来表达关于程序变量值的条件. 该记号被非形式化地描述并通过示例加以刻画.

第1.1节引论

为了从数学上证明一个程序的正确性, 我们必须首先刻画正确本身的含义. 本章我们描述了一种用于刻画命令式程序的预期行为的记号. 这种记号应该归功于C.A.R. Hoare.

执行命令式程序有着改变状态的作用, 直到第7章之前, 我们将状态取为程序变量的值. 为了使用这样的程序, 我们需要建立初始状态, 也就是将一些变量的值设置为有趣的值 (value of interest). 然后我们执行程序. 这将初始状态变换为最终状态. 然后我们检视最终状态里的变量的值来得到预期的结果. 例如, 为了计算

y

除以

x

, 我们可能会将

x

和

y

分别载入程序变量

X

和

Y

. 然后我们可能会执行一个合适的程序 (见第1.4节的例子7) 来将初始状态变换为最终状态以使得变量

Q

和

R

分别存放着商和余数.

第1.2节一种小语言

程序由诸如赋值和条件式等命令构建而成. 术语程序和命令的确可以算是近义词; 前者只会用于表示完整算法的命令. 这里的术语陈述 (statement)用于程序变量上的条件, 其出现于正确性规约之中 (见第1.3节). 这里存在混淆的风险, 因为一些作者将这个词用于命令 (如for-statement [14]).

现在我们描述我们的小语言里的各种命令的句法 (即形式) 和语义 (即意义). 以下约定将会采用:

第1.2.1小节赋值

语义: 状态的改变由将项

E

之值赋给变量

V

完成. 所有的变量都假定具有全局作用域.

第1.2.2小节序列

变量

X

和

Y

之值经由临时变量

R

进行了互换. 这个命令具有将变量

R

之值变为变量

X

之旧值的副作用. {译注: 这个还是这些?}

第1.2.3小节条件式

语义: 如果陈述

S

在当前状态下为真, 那么

C_{1}

被执行. 如果

S

为假, 那么

C_{2}

被执行.

第1.2.4小节

WHILE

命令

语义: 如果陈述

S

在当前状态下为真, 那么

C

被执行, 然后

WHILE

命令重复. 如果

S

为假, 那么什么也不做. 因此,

C

反复执行, 直至

S

的值变为假. 如果

S

永远不变为假, 那么该命令的执行永远不终止.

如果

X

之值非零, 那么其值会减去

2

, 然后进程重复. 这个

WHILE

命令将会终止 (此时

X

有着值

0

), 如果

X

的值是一个非负的偶数. 其他状态下都不会终止.

第1.2.5小节句法总结

第1.2.6小节历史注记

旧的Part II课程Specification and Verification I是基于一种与上述描述类似的语言的, 但具有额外的特性: 块 (带有局部变量),

FOR

命令和数组. 块和

FOR

命令并未添加根本性的新思想, 因此它们将不会被涵盖; 数组使用分离逻辑能够更好地处理 (见第7章). 在旧课程中我使用

BEGIN

和

END

来组合命令, 而在这里我只使用括号. 因此以前我会写

BEGIN C_{1}; C_{2} END

而不是

(C_{1}; C_{2})

. 我提及此事是因为它可能有助于将旧的考试题目作为本课程的练习来重新使用.

第1.3节 Hoare记号

在一篇开创性论文 [13] 里C.A.R. Hoare引入了记号

{P} C {Q}

, 其有时被称为Hoare三元组, 用于刻画一个程序做了什么. 在这样一个Hoare三元组之中:

我们称

{P} C {Q}

为真, 如果每当

C

在某个满足

P

的状态下执行且

C

的执行终止, 那么

C

执行终止的状态满足

Q

例子:

{X = 1} X ≔ X + 1 {X = 2}

. 这里的

P

是

X

之值为

1

这一条件,

Q

是

X

之值为

2

这一条件,

C

是赋值命令

X ≔ X + 1

{X = 1} X ≔ X + 1 {X = 2}

为真. {译注: 这个为真是从语义角度而言的.}

一个表达式

{P} C {Q}

被称为一个部分正确性规约;

P

被称为其前条件而

Q

被称为其后条件.

这样的规约之所以是部分的, 是因为即便

{P} C {Q}

为真,

C

的执行在满足

P

的状态下开始也不必终止. 其所要求的仅是如果

C

终止, 那么

Q

成立.

一种更强的规约是完全正确性规约. 这种规约没有标准的记号. 我们将使用

[P] C [Q]

完全正确性是我们最终感兴趣的, 但通常更容易通过分别建立部分正确性和终止性来证明它.

终止性通常是容易建立的, 但有一些著名的例子并非如此. 例如, 未解决的Collatz猜想与下面的程序是否对

X

的所有值都终止有关 (见下面的练习):

著名数学家Paul Erdős关于Collatz猜想说道: 数学对于这样的问题尚未准备好. 他为其解答提供500美元奖励.

第1.4节一些例子

在以下的例子5, 6, 7中,

T

是永远为真的条件. 在例子3, 4, 7中,

\land

是联结词合取, 即如果

P_{1}

和

P_{2}

是条件, 那么

P_{1} \land P_{2}

是这样的条件, 其为真每当

P_{1}

和

P_{2}

均成立.

这个例子里用到了程序变量

Q

, 读者不应将其与5中所用到的

Q

混淆. 程序变量

Q

(注意字体) 遍历数字, 而后条件

Q

(注意字体) 则遍历陈述. 一般而言, 我们使用

typewriter font

表示特定的程序变量, 而使用

italic font

表示遍历陈述的变量. 尽管这种对于字体的微妙运用乍看上去可能令人迷惑, 但是读者一旦理解之后, 两种Q之间的区分就非常显然了. (即便不看字体, 你也应该能够从上下文中区分它们.)

第1.5节项和陈述

这里用于表达前条件和后条件的记号基于一阶逻辑. 我们只会简要回顾, 因为读者默认已经非常熟悉它了.

以下是原子陈述的例子:

T, F, X = 1, R < Y, X = R + (Y \times Q)

陈述要么为真要么为假. 陈述

T

永远为真, 而陈述

F

永远为假. 陈述

X = 1

为真, 如果

X

之值等于

1

. 陈述

R < Y

为真, 如果

R

之值小于

Y

之值. 陈述

X = R + (Y \times Q)

为真, 如果

X

之值等于

R

之值与

Y

和

Q

之积的和.

陈述由项构建而成, 例如:

X, 1, R, Y, R + (Y \times Q), Y \times Q

项指称着值, 例如数字和字符串, 不像陈述要么为真要么为假. 一些项, 例如

1

和

4 + 5

, 指称着固定的值, 而其他一些项则包含变量, 例如

X, Y, Z

等等, 其值可能会变化. 我们对于项将会使用常规数学记号, 如以下例子所刻画的那样:

X, Y, Z

1, 2, 325

- X, - (X + 1), (X \times Y) + Z

\sqrt{(1 + X^{2})}, X!, \sin (X), rem (X, Y)

T

和

F

是分别总是为真和为假的原子陈述. 其他的原子陈述则由项使用谓词构建而成. 以下是更多的一些例子:

ODD (X), PRIME (3), X = 1, {(X + 1)}^{2} \geq X^{2}

ODD

和

PRIME

是谓词的例子, 而

=

和

\geq

则是中缀谓词的例子. 表达式

X, 1, 3, X + 1, {(X + 1)}^{2}, X^{2}

是项的例子.

复合陈述由原子陈述使用以下逻辑联结词构建而成:

\begin{array}{l} \neg & 否定 \\ \land & 合取 \\ \lor & 析取 \\ \Rightarrow & 推出 \\ \Leftrightarrow & 当且仅当 \end{array}

设

P

和

Q

是陈述, 那么:

第2章 Hoare逻辑

本章讨论了形式化证明的想法. 然后, 我们引入了Hoare逻辑 (或称Floyd-Hoare逻辑) 作为对于程序进行形式化推理的方法.

这个证明由一系列行构成, 每行都是某个公理的实例或者根据之前的行由推理规则推出. 这个证明的最后一行是其所证明的陈述, 也就是

{(X + 1)}^{2} = X^{2} + 2 \times X + 1

为了构造部分正确性规约的形式化证明, 需要公理和推理规则. 这正是Hoare逻辑所提供的. 该演绎系统的形式化表述归功于Hoare [13], 但其中一些基本思想源自Floyd [9].

Hoare逻辑中的证明是一系列行的序列, 其中每一行要么是该逻辑的一条公理, 要么是由前面的行通过该逻辑的一条推理规则推导而来.

构造形式化证明的原因在于试图确保只使用可靠的演绎方法. 有了可靠的公理和推理规则, 我们就可以确信所得出的结论是真的. 另一方面, 如果任何公理或推理规则是不可靠的, 那么就有可能推导出错误的结论; 例如:

\begin{array}{l} 1. & \sqrt{- 1 \times - 1} & = & \sqrt{- 1 \times - 1} & = 的自反性. \\ 2. & \sqrt{- 1 \times - 1} & = & (\sqrt{- 1}) \times (\sqrt{- 1}) & \sqrt{} 之于 \times 的分配律. \\ 3. & \sqrt{- 1 \times - 1} & = & {(\sqrt{- 1})}^{2} & {()}^{2} 的定义. \\ 4. & \sqrt{- 1 \times - 1} & = & - 1 & \sqrt{} 的定义. \\ 5. & \sqrt{1} & = & - 1 & 鉴于 - 1 \times - 1 = 1 . \\ 6. & 1 & = & - 1 & 鉴于 \sqrt{1} = 1 . \end{array}

形式化证明明确指出了为得出结论所使用的公理和推理规则. 人们很容易提出一些看似合理但实际上不可靠的程序推理规则. 计算机程序的正确性证明往往非常复杂, 需要形式化方法来确保其有效性. 因此, 将所使用的推理原则完全显式化是很重要的, 这样才能对其可靠性进行分析.

对于某些应用而言, 正确性尤为重要. 例子包括生命攸关的系统, 如核反应堆控制器, 汽车制动系统, 电传飞控飞机以及软件控制的医疗设备. 曾有一起法律诉讼源于一台癌症治疗设备因软件缺陷导致辐射过量, 造成数人死亡 [15]. 当穷举测试不可能实现时 (几乎总是如此), 形式化正确性证明提供了一种确认程序中不存在缺陷的方法.

本章将解释并举例说明用于程序推理的Hoare演绎系统. 该系统的可靠性和完备性的数学分析将在第4章中讨论.

第2.1节 Hoare逻辑的公理和规则

正如本章开头所讨论的, 一个命题的形式化证明是以该命题为最后一行的一个行序列, 其中每一行要么是一条公理的实例, 要么是由前面的行通过一条推理规则推导而来. 若

S

是一个命题 (无论是普通数学的还是Hoare逻辑的), 我们记

⊢ S

来表示

S

有一个证明. 拥有证明的命题称为定理. 如前所述, 在本讲义中只描述Hoare逻辑的公理和推理规则; 因此, 若

S

是一个数学定理, 我们将直接断言

⊢ S

而不给出任何形式化的论证. 当然, 为了达到完全的严格性, 这些断言必须被证明, 但如何做到这一点的细节假定读者已经了解 (例如通过逻辑与证明课程).

Hoare逻辑的公理在下面通过模式来指定, 这些模式可以被实例化以得到特定的部分正确性规约. Hoare逻辑的推理规则将用如下形式的记号来描述:

\frac{⊢ S_{1} \dots ⊢ S_{n}}{⊢ S}

这是说结论

⊢ S

可以从

⊢ S_{1}, \dots, ⊢ S_{n}

推导而来, 后者是该规则的假设. 这些假设可以全部是Hoare逻辑的定理 (如下面的顺序规则), 也可以是Hoare逻辑定理与数学定理的混合 (如第2.1.2小节中描述的前条件加强规则).

第2.1.1小节赋值公理

赋值公理表达了这样一个事实: 在执行赋值命令

V ≔ E

之后, 变量

V

的值等于执行前表达式

E

的值. 为了将此形式化, 注意到如果一个命题

P

在赋值之后为真, 那么在执行赋值之前, 将

P

中的

V

替换为

E

所得到的命题必须为真. {译注: 这似乎和以下公理所表达的内容方向相反.}

为了形式化地表达这一点, 定义

P [E / V]

以表示将

P

中所有

V

的出现替换为

E

之结果.

P [E / V]

读作

P

with

E

for

V

. 例如,

(X + 1 > X) [Y + Z / X] = ((Y + Z) + 1 > Y + Z)

记住这个记号的方法是消去律

V [E / V] = E

这类比于分式的消去性质

v \times (e / v) = e

Hoare赋值公理

⊢ {P [E / V]} V ≔ E {P}

其中

V

是任意的变量,

E

是任意的表达式,

P

是任意的陈述, 而

P [E / V]

代表将陈述

P

中变量

V

的所有出现都替换为项

E

许多人会感到赋值公理和他们所期望的相反. 两种常见的错误直觉如下:

关于赋值公理容易产生错误直觉这一事实表明, 拥有严格的手段来确立公理和规则的有效性是很重要的. 我们将在后面的第4章中深入讨论这个主题, 届时我们将给出我们这个小型编程语言的形式化语义, 然后证明Hoare逻辑的公理和推理规则是可靠的. 当然, 这一过程只有在我们相信形式化语义本身的正确性的前提下, 才能增强我们对公理和规则的信心. 上述简单的赋值公理对于真实的编程语言是不成立的. 例如, G. Ligler [17] 的工作表明, 它在(现已过时的)语言Algol 60中以六种不同的方式失效.

赋值公理存在一种前向版本, 其有时称为Floyd赋值公理, 因为其对应于应该归功于Floyd [9] 的赋值的原始语义. 在以下规则之中, 存在量化的变量

v

是执行赋值之前的状态 (始状态) 中的

V

之值. 后条件断言了在赋值之后,

V

之值是

E

在初始状态下求得的值 (因而是

E [v / V]

), 并且在初始状态下评估的前条件 (因而是

P [v / V]

) 继续成立.

Floyd赋值公理

⊢ {P} V ≔ E {\exists v . (V = E [v / V] \land P [v / V])}

其中

v

是一个新变量, 即既不等于

V

也没有出现在

P

或

E

中.

译者注记. 之所以

P [v / V]

继续成立, 是因为

V ≔ E

仅仅改变了

V

的值, 其他什么也没改动. 因此,

P

大致上应该仍然成立, 只不过

V

的值要换成旧值

v

一个实例是:

⊢ {X = 1} X ≔ X + 1 {\exists v . (X = (X + 1 [v / X]) \land (X = 1 [v / X]))}

简化这个后条件:

\begin{array}{l} ⊢ {X = 1} X ≔ X + 1 {\exists v . (X = (X + 1 [v / X]) \land (X = 1 [v / X]))} \\ ⊢ {X = 1} X ≔ X + 1 {\exists v . (X = v + 1 \land v = 1)} \\ ⊢ {X = 1} X ≔ X + 1 {\exists v . (X = 1 + 1 \land v = 1)} \\ ⊢ {X = 1} X ≔ X + 1 {X = 1 + 1 \land \exists v . v = 1} \\ ⊢ {X = 1} X ≔ X + 1 {X = 2 \land T} \\ ⊢ {X = 1} X ≔ X + 1 {X = 2} \end{array}

Floyd赋值公理等价于标准的赋值公理, 但是更难于运用, 这是由于其所引入的存在量词. 然而, 这是分离逻辑的重要部分.

Hoare赋值公理与最弱前条件有关 (见第4.3.3小节), 而Floyd赋值公理则与最强后条件有关 (见第4.4.1小节). 以下这些会在刚才提及的小节里得到解释:

\begin{array}{l} Hoare赋值公理: & {wlp (V ≔ E, Q)} V ≔ E {Q} \\ Floyd赋值公理: & {P} V ≔ E {sp (V ≔ E, P)} \end{array}

其中

wlp (C, Q)

和

sp (C, P)

分别代表最弱自由前条件和最强后条件.

我们的小编程语言和真实语言不同的一个方面在于对于赋值命令的右侧表达式的求值不会对于状态施加副作用. 赋值公理的有效性依赖于这个条件. 为了看出这一点, 设我们的语言得到了扩展, 其可以含有形如

(C; E)

的表达式, 其中

C

是一个命令, 而

E

是一个表达式. 这样一种表达式的求值是先执行

C

, 然后对于

E

求值, 最后返回该结果作为

(C; E)

的值. 因此, 对于这种表达式的求值可能会导致由执行

C

引起的副作用. 例如,

(Y ≔ 1; 2)

具有值

2

, 但是其求值也会对于变量

Y

产生副作用, 通过将

1

存储其中. 如果赋值公理应用于像

(C; E)

这样的表达式, 那么其可以用来推导出:

⊢ {Y = 0} X ≔ (Y ≔ 1; 2) {Y = 0}

这是由于

X

压根就没有出现在

Y = 0

之中. 这个显然是错的, 因为在赋值之后

Y

应该具有值

1

第2.1.2小节前条件强化

下一条Hoare逻辑规则允许第18页的i和ii的前条件得到简化. 回忆一下,

\frac{⊢ S_{1} \dots ⊢ S_{n}}{⊢ S}

表示

⊢ S

可由

⊢ S_{1}, \dots, ⊢ S_{n}

推导出来. {译注: 这是句法概念.}

第2.1.3小节后条件弱化

正如之前的规则允许部分正确性规约里的前条件被强化, 以下的规则允许我们对于后条件进行弱化.

例子: 以下是一个小小的形式证明.

\begin{array}{l} 1. & ⊢ {R = X \land 0 = 0} Q ≔ 0 {R = X \land Q = 0} & 根据赋值公理. \\ 2. & ⊢ R = X \Rightarrow R = X \land 0 = 0 & 根据纯粹逻辑. \\ 3. & ⊢ {R = X} Q ≔ 0 {R = X \land Q = 0} & 根据前条件强化. \\ 4. & ⊢ R = X \land Q = 0 \Rightarrow R = X + (Y \times Q) & 根据算术律. \\ 5. & ⊢ {R = X} Q ≔ 0 {R = X + (Y \times Q)} & 根据后条件弱化. \end{array}

第2.1.4小节规约合取与析取

以下两条规则提供了将关于相同命令的不同规约组合起来的方法.

规约合取

\frac{⊢ {P_{1}} C {Q_{1}} ⊢ {P_{2}} C {Q_{2}}}{⊢ {P_{1} \land P_{2}} C {Q_{1} \land Q_{2}}}

规约析取

\frac{⊢ {P_{1}} C {Q_{1}} ⊢ {P_{2}} C {Q_{2}}}{⊢ {P_{1} \lor P_{2}} C {Q_{1} \lor Q_{2}}}

这些规则对于将证明拆成独立的任务而言是有用的. 例如, 其允许通过单独证明

⊢ {P} C {Q_{1}}

和

⊢ {P} C {Q_{2}}

而证明

⊢ {P} C {Q_{1} \land Q_{2}}

剩余的这些规则允许复合命令的性质由其分量的性质推导而来.

第2.1.5小节顺序规则

接下来的规则允许我们由

C_{1}

和

C_{2}

的规约推导出序列

C_{1}; C_{2}

的部分正确性规约.

第2.1.6小节导出顺序规则

第2.1.7小节条件规则

条件规则

\frac{⊢ {P \land S} C_{1} {Q} ⊢ {P \land \neg S} C_{2} {Q}}{⊢ {P} IF S THEN C_{1} ELSE C_{2} {Q}}

第2.1.8小节

WHILE

规则

如果

⊢ {P \land S} C {P}

, 那么我们称: 每当

S

成立,

P

是

C

的一个不变量.

WHILE

规则是说, 如果

P

每当测试条件成立时是

WHILE

命令之体的一个不变量, 那么

P

是整个

WHILE

命令的一个不变量. 换言之, 如果执行

C

一次能够保持

P

的为真, 那么执行

C

任意多次也能够保持

P

的为真.

WHILE

命令也表达了这样的事实, 在一个

WHILE

命令终止之后, 测试条件必然为假 (否则的话, 之前就不会终止).

例子: 根据之前的规则可得:

⊢ {X = R + (Y \times Q)} R ≔ R - Y; Q ≔ Q + 1 {X = R + (Y \times Q)}

因此, 根据前条件强化, 可知

⊢ {X = R + (Y \times Q) \land Y \leq R} R ≔ R - Y; Q ≔ Q + 1 {X = R + (Y \times Q)}

于是, 根据

WHILE

规则, 取

P

为

X = R + (Y \times Q)

, 可以得到

⊢ {X = R + (Y \times Q)} WHILE Y \leq R DO (R ≔ R - Y; Q ≔ Q + 1) {X = R + (Y \times Q) \land \neg (Y \leq R)}

应用赋值公理两次 (以及顺序公理), 容易推导出

⊢ {T} R ≔ X; Q ≔ 0 {X = R + (Y \times Q)}

根据以上两个结果, 以及顺序规则和后条件弱化, 可以推得

⊢ {T} R ≔ X; Q ≔ 0; WHILE Y \leq R DO (R ≔ R - Y; Q ≔ Q + 1) {R < Y \land X = R + (Y \times Q)}

除了

WHILE

规则这个例外, 目前所有描述的公理和规则对于完全正确性和部分正确性都是可靠的. 这是因为我们的小语言中唯一可能不终止的命令就是

WHILE

命令. {译注: 并且, 根据精心(且脆弱)的安排, 如果该语言里的运算和谓词都是完全的, 那么该语言甚至不会抛出异常.} 现在考虑如下证明:

第2.1.9小节

FOR

规则

第2.1.10小节数组

在第2.1.1小节末我们表明了朴素的数组赋值公理

⊢ {P [E_{2} / A (E_{1})]} A (E_{1}) ≔ E_{2} {P}

并不成立, 这是因为对于

A (X)

的改变也可能改变

A (Y), A (Z), \dots

, 鉴于

X

可能等于

Y, Z, \dots

译者注记. 说明一下, 第2.1.1小节末没有讨论数组的事情.

这个问题的解法 (归功于Hoare) 是将数组赋值

A (E_{1}) ≔ E_{2}

处理为通常赋值

A ≔ A {E_{1} \leftarrow E_{2}}

其中项

A {E_{1} \leftarrow E_{2}}

代表一个等同于

A

的数组, 除了

E_{1}

分量被变为具有值

E_{2}

数组赋值公理

⊢ {P [A {E_{1} \leftarrow E_{2}} / A]} A (E_{1}) ≔ E_{2} {P}

其中

A

是一个数组变量,

E_{1}

是一个整数值表达式,

P

是任意的陈述, 而记号

A {E_{1} \leftarrow E_{2}}

代表一个等同于

A

的数组, 只是

E_{1}

处的值为

E_{2}

为了对于数组进行推理, 以下定义了记号

A {E_{1} \leftarrow E_{2}}

意义的公理是必要的.

数组公理

⊢ A {E_{1} \leftarrow E_{2}} (E_{1}) = E_{2}

⊢ E_{1} \neq E_{3} \Rightarrow A {E_{1} \leftarrow E_{2}} (E_{3}) = A (E_{3})

译者注记. 原文这里实际上写的是

E_{1} \neq E_{3} \Rightarrow ⊢ A {E_{1} \leftarrow E_{2}} (E_{3}) = A (E_{3})

但是译者认为这样写并不好.

第3章机械化程序验证

本章描述了一个简单的程序验证器的架构. 其操作相对于Hoare逻辑的规则而澄清.

人们已经进行了许多尝试(并且仍在继续), 试图通过设计系统来自动完成正确性证明, 让这些系统处理在Hoare逻辑中生成形式化证明时那些枯燥而繁琐的部分. 不幸的是, 逻辑学家已经证明, 从原理上讲, 不可能设计出一种判定过程来自动判定任意数学命题的真假 [10]. 然而, 这并不意味着我们无法拥有能够证明许多有用定理的过程. 一般判定过程的不存在仅仅表明, 我们不能期望自动证明一切. 在实践中, 构建一个能够将验证过程中许多枯燥和常规方面机械化的系统是完全可行的. 本章描述了一种常用的实现方法.

尽管不可能自动判定任意命题的真假, 但检验一个任意的形式化证明是否有效却是可能的. 这包括检查证明中每一行出现的结果是否确实是公理, 或者是由前面的行推导出的结论. 由于程序正确性的证明通常非常冗长且枯燥, 手动生成时往往会包含错误. 因此, 即使证明只能在人工辅助下生成, 对其进行机械化检验仍然是有价值的.

第3.1节概览

前一章展示了如何证明

{P} C {Q}

, 方法是证明

C

的各部分之性质, 然后(以合适的证明规则)将它们拼在一起以获得关于

C

本身的预期性质. 例如, 为了证明

⊢ {P} C_{1}; C_{2} {Q}

, 我们首先证明

⊢ {P} C_{1} {R}

和

⊢ {R} C_{2} {Q}

(对于某个合适的

R

而言), 然后根据顺序规则可以推出

⊢ {P} C_{1}; C_{2} {Q}

这种过程被称为前向证明, 因为人们由公理通过规则向前推进到结论. 在实践中, 更为自然的是后向工作: 从表明

{P} C {Q}

的目标开始, 我们生成子目标, 子目标, 如此反复直至问题解决. 例如, 假定我们想要证明:

⊢ {X = x \land Y = y} R ≔ X; X ≔ Y; Y ≔ R {Y = x \land X = y}

那么根据赋值公理和顺序规则, 证明以下子目标就足够了:

⊢ {X = x \land Y = y} R ≔ X; X ≔ Y {R = x \land X = y}

鉴于

⊢ {R = x \land X = y} Y ≔ R {Y = x \land X = y}

. 根据类似的论证, 这个子目标可以被归约为

⊢ {X = x \land Y = y} R ≔ X {R = x \land Y = y}

这显然可由赋值公理推出.

这里所描述的验证系统可以被视为一个证明检查器, 同时它也为证明的生成提供了一定的帮助. 下图给出了该系统的概览.

该系统的输入是一个部分正确性规约, 其中标注了描述变量之间关系的数学陈述. 系统从标注后的规约中生成一组纯数学陈述, 称为验证条件 (即VC). 在3.5节中将会证明, 如果这些验证条件是可证明的, 那么原始规约就可以从Hoare逻辑的公理和规则中推导出来.

验证条件被传递给一个定理证明器程序, 该程序尝试自动地证明它们; 如果证明失败, 则向用户寻求建议. 我们将集中讨论与Hoare逻辑相关的方面, 而对定理证明本身着墨甚少.

当前大量研究的目标是构建能够将缓慢且昂贵的人类专家的参与降到最低的系统. 这可以通过以下途径实现:

下一节将解释验证条件的工作原理. 在3.5节中, 将依据Hoare逻辑的公理和规则来论证其使用的合理性. 除了作为机械化验证系统的基础之外, 验证条件也是手工进行证明的一种有用方式.

第3.2节验证条件

以下各节描述了如何将面向目标的证明风格形式化. 为了证明一个目标

{P} C {Q}

, 需要完成三件事. 这些将在后文中详细解释, 但这里先给出一个简要概述:

我们将证明, 如果能够证明由

{P} C {Q}

生成的所有验证条件 (其中

C

已被适当注解), 则

⊢ {P} C {Q}

由于验证条件只是数学陈述, 可以将上述第2步视为将验证问题编译或翻译为传统数学问题的过程.

第3.3节注解

带注解的命令是指在其中嵌入了陈述 (称为断言) 的命令. 如果在以下位置插入了陈述, 则称该命令是正确注解的:

译者注记. 这个定义会遇到微妙的序列嵌套问题, 但并非不可解决. 不过, 本讲义呈现时, 似乎默认序列一定是摊平的.

正确注解的规约是一个规约

{P} C {Q}

, 其中

C

是正确注解的命令.

第3.4节验证条件生成

本节描述了一个过程, 其为注解过了的部分正确性规约

{P} C {Q}

生成验证条件. 这个过程是

C

上的递归.

例子:

{X = 0} X ≔ X + 1 {X = 1}

的验证条件为

X = 0 \Rightarrow (X + 1) = 1

这显然为真.

条件式

由

{P} IF S THEN C_{1} ELSE C_{2} {Q}

生成的验证条件为

${P \land S} C_{1} {Q}$ 所生成的验证条件
${P \land \neg S} C_{2} {Q}$ 所生成的验证条件

如果

C_{1}; \dots; C_{n}

被正确注解了, 那么 (见第39页) 其必然具有以下两种形式之一:

序列

{P} C1 ;…; C n−1 ; {R} Cn {Q} (其中Cn不是一个赋值) 所生成的验证条件为:
1. ${P} C_{1}; \dots; C_{n - 1} {R}$ 所生成的验证条件
2. ${R} C_{n} {Q}$ 所生成的验证条件
${P} C_{1}; \dots; C_{n - 1}; V ≔ E {Q}$ 所生成的验证条件是由 ${P} C_{1}; \dots; C_{n - 1} {Q [E / V]}$ 所生成的验证条件

例子:

{X = x \land Y = y} R ≔ X; X ≔ Y; Y ≔ R {X = y \land Y = x}

所生成的验证条件是

{X = x \land Y = y} R ≔ X; X ≔ Y {(X = y \land Y = x) [R / Y]}

所生成的验证条件, 这化简一下是

{X = x \land Y = y} R ≔ X; X ≔ Y {X = y \land R = x}

由此生成的验证条件是

{X = x \land Y = y} R ≔ X {(X = y \land R = x) [Y / X]}

所生成的验证条件, 这又可以简化为

{X = x \land Y = y} R ≔ X {Y = y \land R = x}

这生成的唯一的验证条件是

X = x \land Y = y \Rightarrow (Y = y \land R = x) [X / R]

即可以化简为

X = x \land Y = y \Rightarrow Y = y \land X = x

这显然为真.

WHILE

命令的正确注解规约具有形式

{P} WHILE S DO {R} C {Q}

根据第24页的用法, 注解

R

被称为一个不变量.

$WHILE$ 命令

由

{P} WHILE S DO {R} C {Q}

所生成的验证条件为

$P \Rightarrow R$
$R \land \neg S \Rightarrow Q$
由 ${R \land S} C {R}$ 所生成的验证条件

译者注记. 乍看上去, 对于没有注解过的

WHILE

命令的规约

{P} WHILE S DO C {Q}

我们似乎也能够根据

WHILE

命令的规则生成以下验证条件:

$P \land \neg S \Rightarrow Q$
由 ${P \land S} C {P}$ 所生成的验证条件

但问题在于,

P

往往太强了. 从直觉上来说,

P

描述的是

WHILE

循环执行之前的状态, 而命令的目的恰恰在于改变状态. 因此, 这里的注解几乎完全是必要的, 而且难以自动化.

第3.5节验证条件的澄清

本节将证明, 若一个带注解的规约

{P} C {Q}

所生成的验证条件是可证的, 则该规约在Hoare逻辑中也是可证的, 即

⊢ {P} C {Q}

. 这说明验证条件是充分的, 但并不意味着它们是必要的. 事实上, 验证条件是最弱的充分条件, 但我们在此既不对此作更精确的表述, 也不深入讨论细节. 关于前条件的深入研究可参见Dijkstra的著作 [8].

容易证明验证条件不是必要的, 即

{P} C {Q}

的验证条件不可证并不意味着

⊢ {P} C {Q}

不可推导. 例如, 带注解规约

{T} WHILE F DO {F} X ≔ 0 {T}

的验证条件是不可证的, 但该Hoare三元组在Hoare逻辑中是可证的. {译注: 当我们说其在Hoare逻辑中是可证时, 是直接将命令中的注解完全抛弃了的.}

验证条件充分性的论证将对

C

的结构进行归纳. 这类归纳论证包含两个部分. 首先, 证明结论对赋值命令成立. 其次, 证明当

C

不是赋值命令时, 若结论对

C

的各组成命令成立 (这称为归纳假设), 则结论对

C

也成立. 前者称为归纳基础, 后者称为归纳步骤. 由归纳基础和归纳步骤即可得出结论对所有命令成立.

第3.5.1小节赋值

{P} V ≔ E {Q}

唯一的验证条件是

P \Rightarrow Q [E / V]

. 如果这是可证的, 那么鉴于

⊢ {Q [E / V]} V ≔ E {Q}

(赋值公理), 根据前条件强化可以推出

⊢ {P} V ≔ E {Q}

第3.5.2小节条件式

如果

{P} IF S THEN C_{1} ELSE C_{2} {Q}

的验证条件是可证的, 那么

{P \land S} C_{1} {Q}

和

{P \land \neg S} C_{2} {Q}

的验证条件都是可证的. 根据归纳假设, 我们可以假定

⊢ {P \land S} C_{1} {Q}

和

⊢ {P \land \neg S} C_{2} {Q}

. 因此, 根据条件式规则可得

⊢ {P} IF S THEN C_{1} ELSE C_{2} {Q}

第3.5.3小节序列

第3.5.4小节

WHILE

命令

如果

{P} WHILE S DO {R} C {Q}

生成的验证条件是可证的, 那么

⊢ P \Rightarrow R

⊢ (R \land \neg S) \Rightarrow Q

且由

{R \land S} C {R}

所生成的验证条件是可证的. 根据归纳可得

⊢ {R \land S} C {R}

, 因而根据

WHILE

规则有

⊢ {R} WHILE S DO C {R \land \neg S}

. 然后, 根据consequence规则可得

⊢ {P} WHILE S DO C {Q}

第4章可靠性和完备性

本章研究了Hoare逻辑的公理和规则是否正确 (可靠性) 以及是否充分 (完备性) 的问题. 这要求明确地给出编程语言的意义 (语义), 从而能够严格地定义Hoare三元组的语义.

第4.1节语义

一条命令

C

将一个初始状态转换为一个最终状态 (或者不终止). 对于目前所描述的语言, 从一个给定的初始状态出发, 至多只能到达一个终止状态——即命令是确定性的——但后面当我们向语言中加入存储分配时, 情况就不再如此了. 在数学上, 有几种本质上等价的方式来表示命令的意义. 我们将使用关系, 但部分函数也是常用的方式. 使用关系通常与操作语义相关联, 而部分函数则与指称语义相关联, 不过这并不是严格固定的: 指称语义可以使用关系作为指称, 操作语义也可以归纳地定义函数. 事实上, 在下面的第4.1.2节中, 我们给出了一种命令的指称语义, 其中指称就是关系.

各种风格的语义在很大程度上只是表示相同数学思想的不同方式. 某些数学表示更适合某些目的, 而另一些表示则更适合其他目的. 我在下面给出的语义可能与你在之前课程中见过的语义一致, 也可能不一致. 如果它看起来不同, 那么一个很好的练习就是思考它们之间有何关联.

我们将用状态集合上的一个二元关系来表示命令

C

的意义: 在这个关系中,

s_{1}

与

s_{2}

相关联, 当且仅当

C

在状态

s_{1}

下执行后终止于状态

s_{2}

数学上有多种方式来表示关系, 虽然选择哪种并不真正重要, 但在深入具体细节之前, 先简要介绍一下这些不同的表示方式, 可能有助于避免后续的混淆.

集合论的入门书籍通常将关系表示为序对的集合, 即

x

藉由关系

R

与

y

关联当且仅当

(x, y) \in R

. 因此, 集合

X

和

Y

之间的一个二元关系是

X \times Y

的一个子集, 即

R \subseteq X \times Y

或者

R \in 𝒫 (X \times Y)

, 其中

P

是幂集算子. 如果

S

是任意的集合, 那么任何子集

A \subseteq S

都可以由一个函数

f_{A} : S \to {true, false}

刻画, 该函数的定义为

\forall s \in S . f_{A} (s) = true \Leftrightarrow s \in A

f_{A}

被称为

A

的特征函数. 因此, 一个关系

R \subseteq X \times Y

可以由其特征函数

f_{R}

刻画, 其被定义为

\forall x \in X . \forall y \in Y . f_{R} (x, y) = true \Leftrightarrow (x, y) \in R

其中

f_{R} : X \times Y \to {true, false}

. 如果从集合

S

到集合

T

的所有函数之集合记作

S \to T

, 而

Bool

是集合

{true, false}

, 那么

f_{R} \in X \times Y \to Bool

. 你或许可以从之前的课 (例如ML课) 上回忆一下, 接受两个参数或者更多参数的函数可以被curry化, 以使得这些函数每次接受一个参数. 如果我们对于

f_{R}

进行curry化, 那么就会得到函数

f_{R}^{curried}

, 其定义如下:

f_{R}^{curried} x y = f_{R} (x, y)

那么

f_{R}^{curried} : X \to (Y \to Bool)

, 或是

f_{R}^{curried} : X \to Y \to Bool

, 如果我们采取

\to

向右结合的标准约定. 注意到我们也有

f_{R}^{curried} \in X \to 𝒫 (Y)

. {译注: 原文写的是

f_{R}^{curried} \in 𝒫 (X \to Y \to Bool)

, 这肯定不太对, 但是我不确定我修正之后的版本是作者的原意.}

总结一下, 一个关系

R

可以表示为一个序对的集合, 或者是一个将序对映射至布尔值的特征函数, 或者是curry化了的特征函数. 出于历史和风格方面的混合原因 (多少有些随意), 我们将使用curry化特征函数的表示方式来表示命令的语义. 具体而言, 我们将要定义

Csem C s_{1} s_{2}

来表达如果

C

始于状态

s_{1}

, 那么其会终止于状态

s_{2}

. 这里的

Csem

是用于表示

C

的语义的关系, 其被表示为curry化的特征函数. 我们语言中的命令集合将记作

Com

, 而状态集合则记作

State

. 因此,

Csem C : State \to State \to Bool

或是

Csem : Com \to State \to State \to Bool

. 正如之前我们所提到的, 选择将

Csem C

表示为curry化的特征函数而非序对集合, 更多是风格上的考量, 与实质没有太多关系.

令

Var

是陈述, 表达式 (项), 命令中所允许的变量之集合, 令

Val

是变量可以取的值之集合. 不必具体描述变量和值实际上是什么: 例如,

Var

可以是 ASCII 字符的有限字符串的集合,

Val

可以是整数的集合. 一个状态确定每个变量的值, 并且此外可能包含其他信息. 对于我们的小型编程语言, 将状态取为从

Var

到

Val

的函数就足够了. 使用

A \to B

的记法来表示定义域为

A

, 值域 (实则为陪域) 为

B

的函数的集合, 我们定义状态的集合

State

为:

State = Var \to Val

注意以下写法都是等价的:

s \in State

s \in (Var \to Val)

, 以及

s : Var \to Val

. 对于状态

s

中与变量

v

关联的值, 我们有时记成

s (v)

, 有时记成

s v

, 此即应用表示状态

s

的函数于

v

. 尽管目前将状态表示为从变量到值的函数已经足够了, 第7章我们还要为状态加上另一组件, 用于表示指针的内容. 我们将在那一章中扩展

State

的定义. 特定的状态可以使用

λ

记号来定义. 例如, 将

X

映射为

1

Y

映射为

2

, 而其他一切变量映射为

0

的状态可以定义为

λ v . if v = X then 1 else (if v = Y then 2 else 0)

如果

s \in State, v \in Var, n \in Val

, 那么

s [n / v]

表示这样的状态, 其和

s

一样, 除了变量

v

的值为

n

. 因此,

s [n / v]

由以下等式给出:

s [n / v] = λ v^{'} . if v^{'} = v then n else s (v^{'})

例子:

(λ v . if v = X then 1 else (if v = Y then 2 else 0)) [3 / Z]

=

λ v . if v = X then 1 else (if v = Y then 2 else (if v = Z then 3 else 0))

{译注: 这是所谓的外延相等, 或者说指称相等.}

第4.1.1小节表达式和陈述的语义

命令中可能包含表达式或陈述: 表达式出现在赋值的右侧, 而陈述出现在条件式和

WHILE

命令的测试条件中. Hoare三元组的前条件和后条件也是陈述. Hoare逻辑的经典处理建立在一阶逻辑之上, 表达式被视为逻辑中的项, 陈述被视为公式. 你应该在之前的课程中已经熟悉了一阶逻辑的语义, 我不想在这里重复那些内容. 此外, 在现代应用中, 用于书写前条件和后条件的语言有时比一阶逻辑更弱或更强, 例如无量词逻辑 (更弱) 或高阶逻辑 (更强).

为了避免涉及特定逻辑及其语义的细节, 我们假设已给定表达式集合

Exp

和陈述集合

Sta

, 以及定义它们语义的语义函数

Esem

和

Ssem

, 其中:

\begin{array}{rcl} Esem & : & Exp \to State \to Val \\ Ssem & : & Sta \to State \to Bool \end{array}

现在我们给出一些非形式化的讨论和例子来刻画

Esem

和

Ssem

是如何对于特定逻辑定义的. 我们希望从中可以清楚地看出, 更形式化的处理将如何进行. 按照通常的逻辑术语 (例如IB Tripos课程Logic and Proof中所使用的), 我们是在用状态来表示解释函数, 把

Val

作为论域或者说宇宙. 变量的解释通过在状态中查找来实现:

Esem X s = s (X)

{译注: 原文使用的是

X

, 对于这个字体我不敢苟同, 鉴于它应该是一个代表变量的元变量.}
常量获得其通常的数学或逻辑含义:

\begin{array}{rcl} Esem 3 s & = & 3 \\ Ssem T s & = & true \end{array}

{译注: 这里其实我有点问题, 对于数字我的译文一以贯之没有使用其他字体, 但是书中对于项/表达式中的数字是使用所谓的打字机字体的. 不过, 你会发现原文的排版也有一些疏忽, 例如角标的字体都没有顾及到这一点. 总之, 我只是希望字体不要带来困惑.}
复合表达式或陈述是自底而上进行解释的: (通过递归计算得到的)子表达式的值使用合适的数学或逻辑运算组合起来以得到整个表达式的解释. 例如:

\begin{array}{rcl} Esem (- E) s & = & - (Esem E s) \\ Esem (E_{1} + E_{2}) s & = & (Esem E_{1} s) + (Esem E_{2} s) \end{array}

\begin{array}{rcl} Ssem (\neg S) s & = & \neg (Ssem S s) \\ Ssem (E_{1} < E_{2}) s & = & (Esem E_{1} s) < (Esem E_{2} s) \end{array}

{译注: 原文这里写的是

Ssem (S_{1} < S_{2}) s = (Ssem S_{1} s) < (Ssem S_{2} s)

个人认为并不合理, 因为

<

实际上是一个谓词而非逻辑联结词,

S_{1} < S_{2}

应该是一个原子陈述, 而

S_{1}

和

S_{2}

应该是项 (或者说表达式). 换言之, 我们需要用

Esem

来对于这些分量求值.}
其中这些等式左边的符号

-

+

\neg

<

是陈述句法的一部分 (也就是对象语言的一部分), 而右边的相应符号是非形式化的数学记号的一部分 (也就是我们的元语言的一部分). {译注: 更确切地说, 左边的那些符号本身就是句法, 而右边的符号则指称着某种函数. 而且, 最好我们也应该明确区分项和陈述, 不然就会犯下原文这里的错误.} 这是需要仔细琢磨的微妙之处! 量词 (或许会出现在前条件和后条件里, 但是不会出现在命令的测试里) 以标准方式进行解释:

\begin{array}{rcl} Ssem (\forall v . S) s & = & \forall n . Ssem S (s [n / v]) \\ Ssem (\exists v . S) s & = & \exists n . Ssem S (s [n / v]) \end{array}

{译注: 右边的

n

取值于论域, 即

Val

例子:

Ssem (Y < Z + 3) (λ v . if v = X then 1 else (if v = Y then 2 else 0)) = (2 < 0 + 3)

我们希望这足以解释之后要用到的

Esem

和

Ssem

了. 注意到对于任意的

E \in Exp

和

S \in Sta

, 我们有

\begin{array}{rcl} Esem E & : & State \to Val \\ Ssem S & : & State \to Bool \end{array}

第4.1.2小节命令的语义

Csem C s_{1} s_{2}

将自底而上递归定义. 唯一不含有子命令的命令是赋值. 在一次赋值之后, 最终状态

s_{2}

等于初始状态, 不过其中赋值左侧的变量

V

被更新为右侧表达式

E

在初始状态下的值.

Csem (V ≔ E) s_{1} s_{2} = (s_{2} = s_{1} [(Esem E s_{1}) / V])

从初始状态

s_{1}

出发执行顺序组合

C_{1}; C_{2}

能够到达最终状态

s_{2}

, 当且仅当存在一个中间状态

s

, 使得从

s_{1}

执行

C_{1}

可到达

s

, 并且从该中间状态

s

执行

C_{2}

可到达

s_{2}

Csem (C_{1}; C_{2}) s_{1} s_{2} = \exists s . Csem C_{1} s_{1} s \land Csem C_{2} s s_{2}

如果

S

在状态

s_{1}

中为真, 则从

s_{1}

出发执行条件式

IF S THEN C_{1} ELSE C_{2}

能够到达状态

s_{2}

, 当且仅当从

s_{1}

出发执行

THEN

分支

C_{1}

能够到达

s_{2}

. 然而, 如果

S

在状态

s_{1}

中为假, 则从

s_{1}

出发执行该条件式能够到达状态

s_{2}

, 当且仅当从

s_{1}

出发执行

ELSE

分支

C_{2}

能够到达

s_{2}

Csem (IF S THEN C_{1} ELSE C_{2}) s_{1} s_{2} = if (Ssem S s_{1}) then (Csem C_{1} s_{1} s_{2}) else (Csem C_{2} s_{1} s_{2})

如果从初始状态

s_{1}

出发执行

WHILE S DO C

能够到达最终状态

s_{2}

, 那么必然存在有限次的

C

的迭代能够到达

s_{2}

, 并且

S

在所有中间状态中为真, 而在

s_{2}

中为假. 这通过定义一个迭代有限次的(谓词)函数

Iter

来形式化, 进而我们定义:

Csem (WHILE S DO C) s_{1} s_{2} = \exists n . Iter n (Ssem S) (Csem C) s_{1} s_{2}

函数

Iter

是

n

上的递归, 定义如下:

\begin{array}{rcl} Iter 0 p c s_{1} s_{2} & = & \neg (p s_{1}) \land (s_{1} = s_{2}) \\ Iter (n + 1) p c s_{1} s_{2} & = & (p s_{1}) \land (\exists s . (c s_{1} s) \land (Iter n p c s s_{2})) \end{array}

Iter

的第一个参数

n

是迭代的次数. 第二个参数

p

是状态上的谓词, 例如

Ssem S

. 第三个参数

c

是一个curry化的特征函数, 例如

Csem C

. 第四个和第五个参数分别是初状态和终状态. 如果

Num

代表自然数集合

{0, 1, 2, \dots}

, 那么我们有

Iter : Num \to (State \to Bool) \to (State \to State \to Bool) \to State \to State \to Bool

第4.2节 Hoare逻辑的可靠性

Hoare三元组

{P} C {Q}

的意义被定义为

Hsem P C Q

, 其中:

Hsem P C Q = \forall s_{1}, s_{2} . Ssem P s_{1} \land Csem C s_{1} s_{2} \Rightarrow Ssem Q s_{2}

这个定义可以用来表述Hoare逻辑的可靠性. 为了表明可靠性, 我们需要证明赋值公理的所有实例均为真, 并且如果假设为真则由推理规则得到的所有结论为真. 回忆一下赋值公理:

Hoare赋值公理

⊢ {P [E / V]} V ≔ E {P}

其中

V

是任意的变量,

E

是任意的表达式,

P

是任意的陈述, 而

P [E / V]

代表将陈述

P

中变量

V

的所有出现都替换为项

E

为了证明这是可靠的, 我们必须表明对于每个

V, E, P

Hsem (P [E / V]) (V ≔ E) P

展开

Hsem

的定义会将其转换为:

\forall s_{1}, s_{2} . Ssem (P [E / V]) s_{1} \land Csem (V ≔ E) s_{1} s_{2} \Rightarrow Ssem P s_{2}

展开

Csem

的定义会将其转换为:

\forall s_{1}, s_{2} . Ssem (P [E / V]) s_{1} \land (s_{2} = s_{1} [(Esem E s_{1}) / V]) \Rightarrow Ssem P s_{2}

这可以化简为:

\forall s_{1} . Ssem (P [E / V]) s_{1} \Rightarrow Ssem P (s_{1} [(Esem E s_{1}) / V])

这乍看上去可能有点令人困惑, 因为前件和后件里的记号

[\dots / \dots]

有着不同的含义. 前件里的

P [E / V]

指称着将陈述

P

中的变量

V

替换为表达式

E

的结果. 后件里的

s_{1} [(Esem E s_{1}) / V]

指称着状态, 其由更新

s_{1}

以使得

V

之值为

E

在

s_{1}

中的值得到 (所有其他的变量之值保持不变).

关于替换的离题.我们避免了细致刻画表达式和陈述的句法到底是什么, 所以说也不可能证明关于它们的一般性质. 然而, 对于任何理想的定义, 我们会期望:

Ssem (P [E / V]) s = Ssem P (s [(Esem E s) / V])

例如, 取

P

为

X + Y > Z

E

为

X + 1

V

为

Y

, 那么这个等式就变成了:

Ssem ((X + Y > Z) [(X + 1) / Y]) s = Ssem (X + Y > Z) (s [(Esem (X + 1) s) / Y])

既然

Esem (X + 1) s = s (X) + 1

, 于是以上等式变成了:

Ssem ((X + Y > Z) [(X + 1) / Y]) s = Ssem (X + Y > Z) (s [(s (X) + 1) / Y])

对于左边的替换求值就将其归约为了:

Ssem (X + (X + 1) > Z) s = Ssem (X + Y > Z) (s [(s (X) + 1) / Y])

对于

Ssem

求值给出:

(s (X) + (s (X) + 1) > s (Z)) = ((s [(s (X) + 1) / Y]) (X) + (s [(s (X) + 1) / Y]) (Y) > (s [(s (X) + 1) / Y]) (Z))

使用

s [n / v]

, 右边的等式可以化简, 这就给出 {译注: 原文说

X, Y, Z

要不同, 这不大对, 因为它们不是元变量, 而是对象语言中的变量}:

(s (X) + (s (X) + 1) > s (Z)) = (s (X) + (s (X) + 1) > s (Z))

这显然为真, 因为左边和右边是等同的.
尽管这只是一个例子, 其刻画了为什么对于所有的

S, E, V, s

都有

Ssem (S [E / V]) s = Ssem S (s [(Esem E s) / V])

实际上, 如果这个等式并不成立的话, 那么这个替换的定义就很糟糕了——这个等式的确应该当作替换的语义定义!
离题结束.

回到赋值公理的可靠性上来, 回忆一下其等价于对于所有的

P, E, V

, 以下公式成立:

\forall s_{1} . Ssem (P [E / V]) s_{1} \Rightarrow Ssem P (s_{1} [(Esem E s_{1}) / V])

如果之前离题讨论的替换等式成立, 那么这个推出当然也成立. 这是因为, 对于任意的陈述

P

和

Q

, 如果

P = Q

, 那么可以推出

P \Rightarrow Q

除了

WHILE

规则之外的其他Hoare逻辑规则的可靠性几乎都是平凡的, 即便是

WHILE

规则的可靠性也是相当直接的. 我们将会重述规则, 然后给出可靠性证明的提纲.

如果以下公式对于所有的

P, P^{'}, C, Q

均成立:

(\forall s . Ssem P s \Rightarrow Ssem P^{'} s) \land Hsem P^{'} C Q \Rightarrow Hsem P C Q

那么这条规则就是可靠的.
这在以

Hsem

的定义扩展之后就变成了:

(\forall s . Ssem P s \Rightarrow Ssem P^{'} s) \land (\forall s_{1}, s_{2} . Ssem P^{'} s_{1} \land Csem C s_{1} s_{2} \Rightarrow Ssem Q s_{2})

\Rightarrow

(\forall s_{1}, s_{2} . Ssem P s_{1} \land Csem C s_{1} s_{2} \Rightarrow Ssem Q s_{2})

这是以下陈述的一个实例, 如果我们取

p, p^{'}, q, c

分别为

Ssem P, Ssem P^{'}, Ssem Q, Csem C

(\forall s . p s \Rightarrow p^{'} s) \land (\forall s_{1}, s_{2} . p^{'} s_{1} \land c s_{1} s_{2} \Rightarrow q s_{2})

\Rightarrow

(\forall s_{1}, s_{2} . p s_{1} \land c s_{1} s_{2} \Rightarrow q s_{2})

这显然为真.

规约合取

\frac{⊢ {P_{1}} C {Q_{1}} ⊢ {P_{2}} C {Q_{2}}}{⊢ {P_{1} \land P_{2}} C {Q_{1} \land Q_{2}}}

规约析取

\frac{⊢ {P_{1}} C {Q_{1}} ⊢ {P_{2}} C {Q_{2}}}{⊢ {P_{1} \lor P_{2}} C {Q_{1} \lor Q_{2}}}

如果以下公式对于所有的

P, Q, R, C_{1}, C_{2}

为真:

Hsem P C_{1} Q \land Hsem Q C_{2} R \Rightarrow Hsem P (C_{1}; C_{2}) R

那么这条规则就是可靠的.
这在以

Hsem

的定义扩展之后就变成了:

(\forall s_{1}, s_{2} . Ssem P s_{1} \land Csem C_{1} s_{1} s_{2} \Rightarrow Ssem Q s_{2}) \land (\forall s_{1}, s_{2} . Ssem Q s_{1} \land Csem C_{2} s_{1} s_{2} \Rightarrow Ssem R s_{2})

\Rightarrow

(\forall s_{1}, s_{2} . Ssem P s_{1} \land Csem (C_{1}; C_{2}) s_{1} s_{2} \Rightarrow Ssem R s_{2})

这是以下陈述的一个实例, 如果我们展开

Csem (C_{1}; C_{2})

的定义并取

p, q, r, c_{1}, c_{2}

分别为

Ssem P, Ssem Q, Ssem R, Csem C_{1}, Csem C_{2}

(\forall s_{1}, s_{2} . p s_{1} \land c_{1} s_{1} s_{2} \Rightarrow q s_{2}) \land (\forall s_{1}, s_{2} . q s_{1} \land c_{2} s_{1} s_{2} \Rightarrow r s_{2})

\Rightarrow

(\forall s_{1}, s_{2} . p s_{1} \land (\exists s . c_{1} s_{1} s \land c_{2} s s_{2}) \Rightarrow r s_{2})

这显然为真.

条件规则

\frac{⊢ {P \land S} C_{1} {Q} ⊢ {P \land \neg S} C_{2} {Q}}{⊢ {P} IF S THEN C_{1} ELSE C_{2} {Q}}

如果以下公式对于所有的

P, S, C

均为真:

Hsem (P \land S) C P \Rightarrow Hsem P (WHILE S DO C) (P \land \neg S)

那么这条规则就是可靠的.
在以

Hsem

的定义扩展之后, 这就变成了:

(\forall s_{1}, s_{2} . Ssem (P \land S) s_{1} \land Csem C s_{1} s_{2} \Rightarrow Ssem P s_{2})

\Rightarrow

(\forall s_{1}, s_{2} . Ssem P s_{1} \land Csem (WHILE S DO C) s_{1} s_{2} \Rightarrow Ssem (P \land \neg S) s_{2})

使用等式

Ssem (P \land Q) s_{1} = (Ssem P s_{1} \land Ssem Q s_{1})

和

Ssem (P \land \neg Q) s_{2} = (Ssem P s_{2} \land \neg Ssem Q s_{2})

并扩展

Csem (WHILE S DO C)

的定义可以将其转换为:

第4.3节可判定性和完备性

{T} C {F}

为真当且仅当

C

并不终止, 因而既然停机问题是不可判定的, 于是Hoare逻辑也是不可判定的.

可靠性是指, 凡是能用Hoare逻辑的公理和推理规则推导出的Hoare三元组都是真的. 其逆命题, 即完备性, 则是说任何真的Hoare三元组都能用Hoare逻辑的公理和推理规则推导出来. 遗憾的是, 这在一般情况下并不成立.

考虑

{T} X ≔ X {P}

. 根据之前的语义, 此为真当且仅当

Hsem T (X ≔ X) P

为真, 即:

\forall s_{1}, s_{2} . Ssem T s_{1} \land Csem (X ≔ X) s_{1} s_{2} \Rightarrow Ssem P s_{2}

既然

Csem (X ≔ X) s_{1} s_{2} = (s_{2} = s_{1})

且

Ssem T s_{1} = true

, 这可以归约为

\forall s_{1}, s_{2} . (s_{2} = s_{1}) \Rightarrow Ssem P s_{2}

通过特化

s_{1}

和

s_{2}

为

s

, 这又化简为了

\forall s . Ssem P s

, 即

P

为真. 因此, 如果我们能够使用Hoare逻辑推导出任意为真的Hoare三元组, 那么我们就能使用Hoare逻辑推导出断言语言的任何为真的陈述. 绝大多数适用于刻画程序的逻辑都是不完备的 (例如一阶算术), 于是Hoare逻辑也不可能是完备的.

译者注记.

\forall s_{1}, s_{2} . (s_{2} = s_{1}) \Rightarrow Ssem P s_{2}

通过特化推出

\forall s . Ssem P s

是一个单向行为, 但是因为反方向过于明显, 所以说这的确是一个等价. 换言之, 对于断言所使用的逻辑的真陈述

P

, 在Hoare逻辑里

{T} X ≔ X {P}

也是有效的Hoare三元组. 假如Hoare逻辑是完备的, 那么就存在Hoare逻辑的证明可以推出

{T} X ≔ X {P}

, 那么变相就推出了

P

. 对于较强的逻辑而言, 这都是不可能的, 因其是不完备的.

然而, 上述那种完备性之所以不可能实现, 仅仅是因为用于描述前条件和后条件的规约语言本身的不完备性. 如果我们将程序逻辑与规约逻辑分离开来, 那么就有可能构造出一种称为相对完备性 [6] 的概念, 它在一定程度上让我们确信, Hoare逻辑对于我们所讨论的这一小组简单命令的推理是充分的——也就是说, 不存在缺失的公理或规则. 然而事实证明, 即便是这种有限的完备性, 对于许多实际编程语言中存在的构造 (但不包括我们的玩具语言) 而言也可能是不可能的 [5].

我们不打算详细解释Cook等人在相对完备性方面的工作, 因为其中涉及的技术逻辑问题及其直觉解释都相当微妙 [1, 16]. 此外, 这样做将要求我们对表达前条件和后条件的规约语言的句法, 语义和证明理论进行比我们所期望的更为精确的刻画. 不过, 我们将概述其中的关键思想. 在证明相对完备性时所使用的一个概念是最弱前条件. 这一概念不仅在证明相对完备性方面发挥着作用, 它还具有实际应用价值, 包括提供一种改进的验证条件方法 (我们将在后文讨论), 以及作为程序精化理论的基础.

第4.3.1小节相对完备性

我们将通过使用最弱自由前条件来解释相对完备性的思想, 并证明它对我们的小型程序语言成立. 然而, 我们将把其详细定义和分析推迟到第4.3.2节. 在本节中, 我们仅就最弱自由前条件是什么以及它们具有哪些性质 (下文的

P_{1}, P_{2}, P_{3}

) 做出足够的说明, 以便我们能够解释相对完备性.

对于每个命令

C

和陈述

Q

, 我们假定存在一个陈述

wlp (C, Q)

——直觉上它是确保在执行

C

之后

Q

成立的最弱前条件——并且它具有以下性质:

\begin{array}{lcr} ⊢ {wlp (C, Q)} C {Q} & (P_{1}) \end{array}

陈述

wlp (C, Q)

在规约语言中的存在性取决于规约语言是否足够强. 一个强到足以定义

wlp (C, Q)

的语言被称为是有表达力的 (expressive).

算子

wlp

从一个命令和一个陈述构造出另一个陈述, 而陈述是形式语言中的一个句子. 因此

wlp

是由两个句法实体 (一个命令和一个陈述) 构造出一个句法实体 (一个陈述). 我们还假定存在

wlp

的一个语义对应物, 称为

Wlp

, 它作用于命令的意义 (表示状态上的二元关系的函数) 和陈述的意义 (状态上的谓词).

Wlp

是一个curry化的函数:

Wlp : (State \to State \to Bool) \to (State \to Bool) \to State \to Bool

我们假定以下性质将

wlp

和

Wlp

联系起来, 其对所有命令

C

和陈述

Q

成立:

\begin{array}{lcr} Ssem wlp (C, Q) = Wlp (Csem C) (Ssem Q) & (P_{2}) \end{array}

注意这是一个谓词之间的等式. 我们还假定:

\begin{array}{lcr} Hsem P C Q = \forall s . Ssem P s \Rightarrow Wlp (Csem C) (Ssem Q) s & (P_{3}) \end{array}

相对完备性证明的轮廓现在可以概述如下. 假定

{P} C {Q}

为真, 即

Hsem P C Q

为真. 我们将证明陈述

P \Rightarrow wlp (C, Q)

也必定为真——暂时先假定这一点. 如果我们能够证明这个真陈述, 即有

⊢ P \Rightarrow wlp (C, Q)

, 那么通过前条件加强规则和性质

P_{1}

, 就可以由Hoare逻辑推出

⊢ {P} C {Q}

. 因此, Hoare逻辑的完备性是相对于一个能够证明所有形如

P \Rightarrow wlp (C, Q)

的真陈述的神谕机而言的.

译者注记. 大致上,

P_{1}

是说

wlp

在句法上是前条件,

P_{2}

是说

wlp

和

Wlp

是一致的,

P_{3}

是说

Wlp

在语义上是最弱前条件, 我是这样理解的.

译者注记. 神谕机是否会影响soundness? 这似乎是一个微妙的问题.

总结一下: 相对完备性表明, 如果

wlp (C, Q)

在规约语言中是可表达的, 并且存在一个神谕机能够证明形如

P \Rightarrow wlp (C, Q)

的真陈述, 那么任何为真的Hoare三元组

{P} C {Q}

都可以使用Hoare逻辑来证明.

我们现在再次梳理相对完备性的论证, 但更为详细, 展示假定

P_{2}

和

P_{3}

是如何使用的. 回忆一下:

\begin{array}{lcr} Ssem wlp (C, Q) = Wlp (Csem C) (Ssem Q) & (P_{2}) \end{array}

\begin{array}{lcr} Hsem P C Q = \forall s . Ssem P s \Rightarrow Wlp (Csem C) (Ssem Q) s & (P_{3}) \end{array}

假定对于任意

C

和

Q

wlp (C, Q)

在规约语言中是可表达的, 并且假定对于任意

P, C, Q

, 存在一个神谕机能够证明形如

P \Rightarrow wlp (C, Q)

的真陈述——即如果

\forall s . Ssem (P \Rightarrow wlp (C, Q)) s

(陈述为真), 则神谕机给出

⊢ P \Rightarrow wlp (C, Q)

(陈述得证).

Hoare三元组

{P} C {Q}

为真, 按照我们的语义, 意味着

Hsem P C Q

为真. 如果这成立, 则由上面假定的

P_{3}

\forall s . Ssem P s \Rightarrow Wlp (Csem C) (Ssem Q) s

然后由假定的性质

P_{2}

\forall s . Ssem P s \Rightarrow Ssem wlp (C, Q) s

虽然我们没有完全定义规约语言, 但我们至少假定它包含一个中缀符号

\Rightarrow

, 其含义是逻辑后承, 因此从上面的陈述我们可以推出:

\forall s . Ssem (P \Rightarrow wlp (C, Q)) s

即陈述

P \Rightarrow wlp (C, Q)

为真. 现在我们使用为这种形式的公式所假设的神谕机来证明

⊢ P \Rightarrow wlp (C, Q)

, 因此由假设的性质

P_{1}

和前条件加强规则, 我们可以证明

⊢ {P} C {Q}

为了完成上述概要, 我们必须定义

wlp

和

Wlp

并证明性质

P_{1}, P_{2}, P_{3}

. Hoare逻辑的公理和规则将被用于证明

P_{1}

, 而它们能够证明

P_{1}

这一事实, 正是其完备性的本质所在.

第4.3.2小节句法和语义最弱前条件

译者注记. 这一小节的主要内容是

Wlp

的定义, 以及表述和证明了

Wlp

的一些性质, 这些下一小节要用到. 并且, 你会发现这些性质实际上正是为了配合下一小节而如此表述的.

如果

P \Rightarrow Q

, 我们说

P

比

Q

强, 对偶地,

Q

比

P

弱. 命令

C

相对于后条件

Q

的最弱前条件记作

wp (C, Q)

, 其是满足

[wp (C, Q)] C [Q]

的最弱谓词. 注意到这和完全正确性相关联. 部分正确性的相应概念是最弱自由前条件, 记作

wlp (C, Q)

: 陈述

wlp (C, Q)

是满足

{wlp (C, Q)} C {Q}

的最弱谓词. 本章我们只会使用最弱自由前条件. 其关键性质是

P_{1}

, 即

⊢ {wlp (C, Q)} C {Q}

, 以及对于所有的

P

都有

{P} C {Q} \Rightarrow (P \Rightarrow wlp (C, Q))

这些性质可以更为精确地表述为单一等式:

{P} C {Q} = (P \Rightarrow wlp (C, Q))

我们可以很容易地看出来这个等式与刚才提及的关键性质是等价的, 只需使用前条件加强规则和

\Rightarrow

的自反性.

译者注记. 这里没有看上去这么简单, 我不确定作者想表达什么. 但是这个等价需要神谕机, 或者说Hoare逻辑的(相对)完备性.

如果规约语言 (即前条件和后条件的语言) 足够强以表达所有命令

C

和后条件

Q

的最弱自由前条件, 那么其就被称为有表达力的. 既然我们还没有说规约语言是什么, 那么我们对于表达力也就不好说什么.

我们可以藉由我们的语义定义谓词上的语义算子

Wlp

: 这是谓词转换器 [7] 的一个例子.

Wlp c q = λ s . \forall s^{'} . c s s^{'} \Rightarrow q s^{'}

回忆一下

Hsem

的定义:

Hsem P C Q = \forall s_{1}, s_{2} . Ssem P s_{1} \land Csem C s_{1} s_{2} \Rightarrow Ssem Q s_{2}

我们可以轻易证明性质

P_{3}

, 即

Hsem P C Q = \forall s . Ssem P s \Rightarrow Wlp (Csem C) (Ssem Q) s

P_{3}

可由

Hsem

和

Wlp

的定义推出, 通过在以下逻辑事实中取

p, c, q

分别为

Ssem P, Csem C, Ssem Q

得到.

(\forall s_{1}, s_{2} . p s_{1} \land c s_{1} s_{2} \Rightarrow q s_{2}) = (\forall s . p s \Rightarrow (λ s . \forall s^{'} . c s s^{'} \Rightarrow q s^{'}) s)

为了证明

P_{1}

和

P_{2}

, 我们需要下列等式, 其可由

Wlp

的定义推出.

\begin{array}{rcl} Wlp (Csem (V ≔ E)) q & = & λ s . q (s [(Esem E s) / V]) \\ Wlp (Csem (C_{1}; C_{2})) q & = & λ s . Wlp (Csem C_{1}) (Wlp (Csem C_{2}) q) s \\ Wlp (Csem (IF S THEN C_{1} ELSE C_{2})) q & = & λ s . if (Ssem S s) then (Wlp (Csem C_{1}) q s) else (Wlp (Csem C_{2}) q s) \\ Wlp (Csem (WHILE S DO C)) q & = & λ s . \forall n . IterWlp n (Ssem S) (Csem C) q s \\ IterWlp 0 p c q s & = & \neg (p s) \Rightarrow (q s) \\ IterWlp (n + 1) p c q s & = & (p s) \Rightarrow (Wlp c (IterWlp n p c q) s) \end{array}

{译注:

(IterWlp n p c q s)

为真的含义应该是从状态

s

出发, 如果恰好执行

n

次循环体并退出, 那么

q s

为真, 其中

p

是循环条件

S

的语义,

c

是循环体命令

C

的语义. 注意一下, 提前或者延迟退出循环体都会导致这个谓词自动为真.}

第4.3.3小节句法前条件和可表达性

译者注记. 这一小节递归定义了

wlp

, 并归纳证明了

wlp

的性质, 也就是

P_{1}

, 以及

wlp

和

Wlp

的协调, 也就是

P_{2}

. 可能用到前一小节的结果, 当然前一小节的定义肯定是要使用的.

现在我们讨论如何以性质

P_{1}

和

P_{2}

定义陈述

wlp (C, Q)

, 即

\begin{array}{lcr} ⊢ {wlp (C, Q)} C {Q} & (P_{1}) \end{array}

\begin{array}{lcr} Ssem wlp (C, Q) = Wlp (Csem C) (Ssem Q) & (P_{2}) \end{array}

请注意,

wlp

是在句法东西 (命令和陈述) 上操作的, 而

Wlp

则是在语义东西 (状态上的数学函数, 代表命令和陈述的意义) 上操作的.

我们将在

C

上递归定义

wlp (C, Q)

, 然后藉由

C

上的结构归纳澄清

P_{1}

和

P_{2}

C

为赋值, 序列或是条件式的情形是直接的.

wlp (V ≔ E, Q) = Q [E / V]

如果

C

为

V ≔ E

, 那么

P_{1}

直接就是赋值公理, 而根据第61页所讨论的等式

Wlp (Csem (V ≔ E)) q = λ s . q (s [(Esem E s) / V])

P_{2}

为等式

Ssem (Q [E / V]) s = Ssem Q (s [(Esem E s) / V])

这不过就是第53页的关于替换的离题所澄清的.

wlp (C_{1}; C_{2}, Q) = wlp (C_{1}, wlp (C_{2}, Q))

假定对于任意的

Q

P_{1}

和

P_{2}

对于

C_{1}

和

C_{2}

均成立, 那么

⊢ {wlp (C_{2}, Q)} C_{2} {Q}

⊢ {wlp (C_{1}, wlp (C_{2}, Q))} C_{1} {wlp (C_{2}, Q)}

于是根据顺序规则可以得到

P_{1}

, 即

⊢ {wlp (C_{1}, wlp (C_{2}, Q))} C_{1}; C_{2} {Q}

为了证明

P_{2}

, 当

C

为

C_{1}; C_{2}

时, 注意到这种情况下的

P_{2}

为

\begin{array}{cl} Ssem wlp (C_{1}; C_{2}, Q) \\ = & Ssem wlp (C_{1}, wlp (C_{2}, Q)) \\ = & Wlp (Csem (C_{1}; C_{2})) (Ssem Q) \\ = & Wlp (λ s_{1}, s_{2} . \exists s . (Csem C_{1} s_{1} s) \land (Csem C_{2} s s_{2})) (Ssem Q) \\ = & λ s_{1} . \forall s_{2} . (\exists s . (Csem C_{1} s_{1} s) \land (Csem C_{2} s s_{2})) \Rightarrow (Ssem Q s_{2}) \\ = & λ s_{1} . \forall s, s_{2} . (Csem C_{1} s_{1} s) \land (Csem C_{2} s s_{2}) \Rightarrow (Ssem Q s_{2}) \end{array}

(未完待续)

wlp (IF S THEN C_{1} ELSE C_{2}, Q) = (S \land wlp (C_{1}, Q)) \lor (\neg S \land wlp (C_{2}, Q))

注意到

(S \land S_{1}) \lor (\neg S \land S_{2})

的含义是

if S then S_{1} else S_{2}

. 前者是为了强调我们对于规约语言的假定仅是布尔运算符

\neg, \land, \lor

的存在. 注意到根据布尔代数以及

wlp (IF S THEN C_{1} ELSE C_{2}, Q)

的定义, 我们有

\begin{array}{rcl} S \land wlp (IF S THEN C_{1} ELSE C_{2}, Q) & = & S \land wlp (C_{1}, Q) \\ \neg S \land wlp (IF S THEN C_{1} ELSE C_{2}, Q) & = & \neg S \land wlp (C_{2}, Q) \end{array}

根据归纳假设和前条件强化, 可以得到

⊢ {S \land wlp (C_{1}, Q)} C_{1} {Q}

⊢ {\neg S \land wlp (C_{2}, Q)} C_{2} {Q}

{译注: 原文忘了加

⊢

, 译者将其补上.} 代入之前的等式, 并利用条件规则, 可以获得

⊢ {wlp (IF S THEN C_{1} ELSE C_{2}, Q)} IF S THEN C_{1} ELSE C_{2} {Q}

这就是条件式的性质

P_{1}

. {译注: 这里作者的措辞存在疏漏, 作者说是利用布尔代数得到了等式, 然后代入. 严格说来, 这并不正确, 因为布尔代数是语义层面的事情. 不过, 句法层面我们也有分配律等手段可用, 这和语义层面是一样的, 所以论证可以修补成正确的形式.} 性质

P_{2}

为

\begin{array}{cl} Ssem ((S \land wlp (C_{1}, Q)) \lor (\neg S \land wlp (C_{2}, Q))) \\ = & Wlp (Csem (IF S THEN C_{1} ELSE C_{2})) (Ssem Q) \end{array}

第4.4节藉由

wlp

生成验证条件

最弱前条件提供了一种理解和改进验证条件的方式. 回忆一下性质

P_{1}

, 即

⊢ {wlp (C, Q)} C {Q}

. 为了证明

{P} C {Q}

为真, (根据前条件强化)证明

⊢ P \Rightarrow wlp (C, Q)

就足够了. 因此, 我们可以将

P \Rightarrow wlp (C, Q)

视为对于目标

{P} C {Q}

而言的单独一条超级验证条件, 其无需对于

C

进行注解即可生成! 如果

C

不含有循环, 即不含有

WHILE

命令, 那么这就能很好地运转. 如果

C

的确含有

WHILE

命令, 那么

wlp (C, Q)

将会是无限的陈述. 证明这样的陈述通常会涉及用归纳法证明本质上就是某个不变式的验证条件的东西. 因此找不变式是无法回避的! 然而, 可以用最弱前条件的思想来既解释又改进验证条件方法. 为了看出它如何解释验证条件, 回忆第41页, 由

{P} C_{1}; \dots; C_{n - 1}; V ≔ E {Q}

生成的验证条件是:

{P} C_{1}; \dots; C_{n - 1} {Q [E / V]}

(的验证条件), 也就是

{P} C_{1}; \dots; C_{n - 1} {wlp (V ≔ E, Q)}

(的验证条件). 我们可以推广这一观察, 以减少序列中所需的标注数量, 做法是只要求在不是无循环的 (即包含

WHILE

命令的) 命令之前加标注, 然后修改序列的验证条件:

序列

{P} C1 ;…; C n−1 ; {R} Cn {Q} 其中Cn包含一个WHILE命令, 由其所生成的验证条件为:
1. ${P} C_{1}; \dots; C_{n - 1} {R}$ 所生成的验证条件
2. ${R} C_{n} {Q}$ 所生成的验证条件
${P} C_{1}; \dots; C_{n - 1}; C_{n} {Q}$ 其中 $C_{n}$ 无循环, 由其所生成的验证条件为 ${P} C_{1}; \dots; C_{n - 1} {wlp (C_{n}, Q)}$ 所生成的验证条件.

第4.4.1小节最强后条件

最弱前条件是由后条件开始反向计算的. 存在一个最强后条件的对偶理论, 其是自前条件正向计算的. 最强后条件具有性质

⊢ {P} C {sp (C, P)}

, 并且是最强的, 意即对于任意的

Q

, 如果

⊢ {P} C {Q}

, 那么

⊢ sp (C, P) \Rightarrow Q

. 从直觉上说,

sp (C, P)

是在由

P

所描述的初始状态下对于执行

C

之后的状态的符号表示. 对于赋值而言:

sp (V ≔ E, P) = \exists v . (V = E [v / V] \land P [v / V])

存在量化变量

v

是

V

在执行赋值之前的初始状态中的值. 最强后条件表达了在赋值之后,

V

之值是

E

在初始状态下求得的值 (因而是

E [v / V]

), 而前条件在初始状态下评估 (因而是

P [v / V]

) 继续成立. 因此, 如果初始状态由陈述

(V = v) \land P

符号地表示, 那么执行

V ≔ E

之后的状态可由

(V = E [v / V]) \land P [v / V]

符号地表示.

对于无循环命令

C

sp (C, P)

相当于从符号状态

P

开始对于

C

进行符号执行. 符号执行的一个优点在于其允许对于到目前为止的状态的表示进行on-the-fly式的化简,

第5章完全 (total) 正确性

本章Hoare逻辑的公理和规则被扩展到了完全正确性, 其给出了完全正确性规约的验证条件.

在1.3节中, 我们引入了记号

[P] C [Q]

来表示完全正确性规约, 即每当

C

在满足

P

的状态下执行时, 它将终止于一个满足

Q

的状态. 在描述

WHILE

规则的那一节 (第2.1.8节) 末尾, 我们已经表明该规则对于完全正确性规约不是可靠的. 这是因为

WHILE

命令可能引入非终止性. 其他命令都不会引入非终止性, 因此Hoare逻辑的规则可以继续使用.

第5.1节非循环命令

完全正确性的前条件加强

\frac{⊢ P \Rightarrow P^{'} ⊢ [P^{'}] C [Q]}{⊢ [P] C [Q]}

完全正确性的后条件弱化

\frac{⊢ [P] C [Q^{'}] ⊢ Q^{'} \Rightarrow Q}{⊢ [P] C [Q]}

完全正确性的规约合取

\frac{⊢ [P_{1}] C [Q_{1}] ⊢ [P_{2}] C [Q_{2}]}{⊢ [P_{1} \land P_{2}] C [Q_{1} \land Q_{2}]}

完全正确性的规约析取

\frac{⊢ [P_{1}] C [Q_{1}] ⊢ [P_{2}] C [Q_{2}]}{⊢ [P_{1} \lor P_{2}] C [Q_{1} \lor Q_{2}]}

完全正确性的顺序规则

\frac{⊢ [P] C_{1} [Q] ⊢ [Q] C_{2} [R]}{⊢ [P] C_{1}; C_{2} [R]}

完全正确性的条件规则

\frac{⊢ [P \land S] C_{1} [Q] ⊢ [P \land \neg S] C_{2} [Q]}{⊢ [P] IF S THEN C_{1} ELSE C_{2} [Q]}

这些规则从形式上来说和相应的Hoare逻辑规则等同, 除了使用方括号而非花括号. 因此, 显然以下是可靠 (valid) 的导出规则.

\frac{⊢ {P} C {Q}}{⊢ [P] C [Q]}, 如果 C 不含有 WHILE 命令

{译注: 以我之见, 这与其说是导出规则, 不如说是兼容规则 (admissible rule).}

第5.2节赋值的终止性

注意到完全正确性的赋值公理陈述了赋值命令总是终止, 这隐式地假定了表达式中的所有函数应用都会终止. 如果函数可以递归定义, 那么或许并非如此. 例如, 考虑赋值

X ≔ fact (- 1)

, 其中

fact (n)

被递归定义为

fact (n) = IF n = 0 THEN 1 ELSE n \times fact (n - 1)

通常也假定诸如

1 / 0

这样错误的表达式也不会造成任何问题. 绝大多数编程语言遇到除以零时都会导致错误停下. 然而, 在我们的逻辑里, 可以推出

⊢ [T] X ≔ 1 / 0 [X = 1 / 0]

即赋值

X ≔ 1 / 0

总是能终止于一个条件

X = 1 / 0

成立的状态. 这假定

1 / 0

指称着某个

X

可以具有的值. 存在两种可能性:

另一种处理错误的方法在于扩展命令的语义, 允许错误和状态一样作为结果. 这种方法用在第7章以处理内存错误, 但是类似的想法也能用来处理表达式求值错误 (尽管代价是语义更为复杂).

第5.3节用于完全正确性的

WHILE

规则

WHILE

命令是我们这个小语言中唯一可能导致不终止的命令, 因此也是唯一具有非平凡终止规则的命令.

WHILE

规则用于完全正确性的核心思想是: 要证明

WHILE S DO C

能够终止, 必须证明某个非负量在

C

的每次迭代中都会减少. 这个递减的量称为变式量 (variant). {译注: 我感觉很多人也将其称为终止度量.} 在下面的规则中, 变式量为

E

, 而它递减的事实通过一个辅助变量

n

来刻画. 一个额外的假设

⊢ P \land S \Rightarrow E \geq 0

确保了变式量是非负的.

第5.4节终止规约

正如第1.3节已经讨论过了的, 部分正确性和完全正确性之间的关系可以非正式地表述为以下等式:

完全正确性 = 终止性 + 部分正确性

第5.5节终止性的验证条件

第5.6节验证条件生成

第6章程序精化

Floyd-Hoare逻辑是一种证明现有程序满足其规约的方法. 它也可以作为将规约精化为程序的基础——即作为一种程序设计方法论的基础.

第6.1节引论

程序员的任务可以被看作: 给定一个由前条件

P

和后条件

Q

组成的规约, 然后构造出一个命令

C

, 使得

[P] C [Q]

成立.

精化理论提出了从规约

P

和

Q

计算出程序

C

的规则. 一个关键思想来自芬兰的Ralph Back (后来被Joseph Morris和Carroll Morgan各自独立地重新发现), 即引入一类新的程序构造, 称为规约. 这些构造在句法上扮演与命令相同的角色, 但它们不可直接执行, 不过它们能保证在给定的前条件下达成给定的后条件. 由此产生的广义编程语言包含纯规约, 纯代码以及二者的混合体. 这样的语言被称为宽谱语言.

本章采用的方法遵循Morgan所发展的精化风格, 但其基础是Floyd-Hoare逻辑, 而非Dijkstra的最弱前条件理论 (见4.3.3节). 与传统方法相比, 这一基础更加具体和句法化: 规约被等同于其所有可能实现的集合, 精化则被表示为对普通命令集合的操作. 这种方法旨在利用前面各章所引入的记号和概念工具, 传达 (Morgan风格的) 精化的外观和感觉.

记号

[P, Q]

将用于表示规约, 因此:

[P, Q] = {C | ⊢ [P] C [Q]}

精化过程将由一系列步骤组成, 这些步骤通过系统性的设计决策逐步缩小可能实现的集合, 直到达到唯一的实现. 因此, 从规约

S

到实现

C

的精化具有如下形式:

S \supseteq S_{1} \supseteq S_{2} \supseteq \dots \supseteq S_{n} \supseteq {C}

初始规约

S

具有

[P, Q]

的形式, 每个中间规约

S_{i}

都是通过对其前驱

S_{i - 1}

应用一条精化律而得到的.

在文献中,

S \supseteq S^{'}

通常写作

S ⊑ S^{'}

. 这里使用

\supseteq

而非更抽象的

⊑

, 反映了精化作为逐步缩小实现集合这一具体解释.

Hoare逻辑

第1章 程序规约

第1.1节 引论

第1.2节 一种小语言

第1.2.1小节 赋值

第1.2.2小节 序列

第1.2.3小节 条件式

第1.2.4小节 WHILE命令

第1.2.5小节 句法总结

第1.2.6小节 历史注记

第1.3节 Hoare记号

第1.4节 一些例子

第1.5节 项和陈述

第2章 Hoare逻辑

第2.1节 Hoare逻辑的公理和规则

第2.1.1小节 赋值公理

第2.1.2小节 前条件强化

第2.1.3小节 后条件弱化

第2.1.4小节 规约合取与析取

第2.1.5小节 顺序规则

第2.1.6小节 导出顺序规则

第2.1.7小节 条件规则

第2.1.8小节 WHILE规则

第2.1.9小节 FOR规则

第2.1.10小节 数组

第3章 机械化程序验证

第3.1节 概览

第3.2节 验证条件

第3.3节 注解

第3.4节 验证条件生成

第3.5节 验证条件的澄清

第3.5.1小节 赋值

第3.5.2小节 条件式

第3.5.3小节 序列

第3.5.4小节 WHILE命令

第4章 可靠性和完备性

第4.1节 语义

第4.1.1小节 表达式和陈述的语义

第4.1.2小节 命令的语义

第4.2节 Hoare逻辑的可靠性

第4.3节 可判定性和完备性

第4.3.1小节 相对完备性

第4.3.2小节 句法和语义最弱前条件

第4.3.3小节 句法前条件和可表达性

第4.4节 藉由wlp生成验证条件

第4.4.1小节 最强后条件

第5章 完全 (total) 正确性

第5.1节 非循环命令

第5.2节 赋值的终止性

第5.3节 用于完全正确性的WHILE规则

第5.4节 终止规约

第5.5节 终止性的验证条件

第5.6节 验证条件生成

第6章 程序精化

第6.1节 引论

第6.2节 精化律

第6.3节 一个例子

第6.4节 一般评注

第7章 指针和局部推理

第7.1节 指针操纵构造

第7.2节 例子: 反转链表

第7.3节 分离逻辑断言

第7.3.1小节 指向关系: E↦F

第7.4节 语义和分离逻辑

第1章程序规约

第1.1节引论

第1.2节一种小语言

第1.2.1小节赋值

第1.2.2小节序列

第1.2.3小节条件式

第1.2.4小节 $WHILE$ 命令

第1.2.5小节句法总结

第1.2.6小节历史注记

第1.4节一些例子

第1.5节项和陈述

第2.1.1小节赋值公理

第2.1.2小节前条件强化

第2.1.3小节后条件弱化

第2.1.4小节规约合取与析取

第2.1.5小节顺序规则

第2.1.6小节导出顺序规则

第2.1.7小节条件规则

第2.1.8小节 $WHILE$ 规则

第2.1.9小节 $FOR$ 规则

第2.1.10小节数组

第3章机械化程序验证

第3.1节概览

第3.2节验证条件

第3.3节注解

第3.4节验证条件生成

第3.5节验证条件的澄清

第3.5.1小节赋值

第3.5.2小节条件式

第3.5.3小节序列

第3.5.4小节 $WHILE$ 命令

第4章可靠性和完备性

第4.1节语义

第4.1.1小节表达式和陈述的语义

第4.1.2小节命令的语义

第4.3节可判定性和完备性

第4.3.1小节相对完备性

第4.3.2小节句法和语义最弱前条件

第4.3.3小节句法前条件和可表达性

第4.4节藉由 $wlp$ 生成验证条件

第4.4.1小节最强后条件

第5章完全 (total) 正确性

第5.1节非循环命令

第5.2节赋值的终止性

第5.3节用于完全正确性的 $WHILE$ 规则

第5.4节终止规约

第5.5节终止性的验证条件

第5.6节验证条件生成

第6章程序精化

第6.1节引论

第6.2节精化律

第6.3节一个例子

第6.4节一般评注

第7章指针和局部推理

第7.1节指针操纵构造

第7.2节例子: 反转链表

第7.3节分离逻辑断言

第7.3.1小节指向关系: $E \mapsto F$

第7.4节语义和分离逻辑