CHAPTER 12 Hoare Logic: Verifying Imperative Programs

从上一章节两个维度前进一步。

• 从函数式转为命令式语言
• 回到对深度一致性（deep correctness）性质的证明，而非缺乏类型相关的崩溃

尽管如此，基本的证明结构最终还是一样的，因为我们再一次证明了转移系统的不变量（invariants of transition systems）（跳跃读，需要补 Chap4 5）。

An Imperative Language with Memory

从定义具有无限可变堆（infinite mutable heap）的命令行语言开始。出于一些原因，mix 了语法和语义。在程序的特定部分，我们包含了表达程序状态（program state）的断言（assertion），用 heap \(h\) 和 variable valuation \(v\) 表示。

\[ \begin{aligned} \mathbf{Numbers} \quad & n \in \mathbb{N} \\ \mathbf{Variables} \quad & x \in \mathbf{Strings} \\ \mathbf{Expressions} \quad & e ::= n|x|e+e|e-e|e \times e | *[e] \\ \mathbf{Boolean} \quad \mathbf{expressions} \quad & b ::= e=e | e < e \\ \mathbf{Commands} \quad & c ::= \mathbf{skip} | x \leftarrow e |*[e] \leftarrow e | c;c \\ & \qquad | \ \mathbf{if} \ b \ \mathbf{then} \ c \ \mathbf{else} \ c \\ & \qquad | \ \{ a \} \ \mathbf{while} \ b \ \mathbf{do} \ c \ | \ \mathbf{assert}(a) \end{aligned} \]

循环在其语法中产生了一个额外的断言，实际上我们将在语言语义中忽略它，但它将成为我们将要学习的证明技术的重要部分，特别是在自动化它的过程中。表达式具有标准的递归语义，这里应该说的是\(\{ a \} \ \mathbf{while} \ b \ \mathbf{do} \ c \ | \ \mathbf{assert}(a)\)这部分。

语义部分描述：（待添加公式）

通过增加线程堆复杂性，完成了大步骤的语义（big——step semantics）。

先尝试 Pass 这一部分。直接推理操作语义可能会很乏味，所以开发一些自动证明程序正确性的机制。

Hoare Triples

如同其他系统一样（有待研究前面的内容？），定义一个语法谓词（syntactic predicate）并一劳永逸地证明它。谓词被写成\(\{P\}c\{Q\}\)地的形式，该形式被称为Hoare triple，按这种谓词的实现称为Hoare logic。

• \(c\)，形式化的命令 command
• \(P\)，前状态 precondition（执行\(c\)之前计算机的状态）。
• \(Q\)，后状态 postcondition （执行之后的状态）。

规则解释

• skip rule. 跳过规则
• assignment rule. 赋值规则
  • 前状态：\(\{P\}\)
  • 过程为：\(x \leftarrow e\)
  • 后状态（这个不大能理解）： \(\{ \lambda(h,v). \ \exists v’. P(h,v’) \land v = v’[x \mapsto [e] (h.v’) ]\}\)
• memory-write rule. 内存写规则

• model sequence rule. 顺序执行规则（这个用来表示非常的方便）

  \[\dfrac{\{P\}c_1\{Q\} \quad \{Q\}c_2\{R\}}{ \{P\}c_1;c_2\{R\} }\]

• condition rule. 排序规则

  从基本的 sequence 方法开始，变动两个地方。其一是由于子命令再测试表达式不同结果后运行，要扩展 precondition。另一方面，由于可能执行任一段子代码，我们不考虑他们的后置条件（看代码稍微能理解些了）。

• 循环规则
• command——specific 规则

• One more essential rule 跟前后条件强弱相关。

上述这些规则（个人理解，这些就是 Axiom 公理）结合在一起是完整的（完备的？complete），任何关于 pre-post 条件对的 command 都是可证的（这里又回到了命令表示？）。完整证明是通过 Coq 完成的。

（机翻）自动证明过程基本思路：首先尝试应用丁聪语法树构造函数（比如 assignment 或 loop rule）。如果规则和目标一致，则递归下去。否则，应用后果规则将后置条件替换为匹配规则中的后置条件； 请注意，所有规则都接受任意形状的前提条件，因此我们实际上不需要做任何工作来按摩前提条件。经过这样的步骤之后，可以确保现在适用“基本”规则。

介绍 Hoare logic 的结尾部分，思考how it brings to bear some more of the general principles that we have met before.

Small-Step Semantics

Transition-System Invariants from Hoare Triples