霍尔逻辑

霍尔逻辑，是一种证明程序正确性的形式化系统。

该系统的目的是提供一组逻辑规则，允许使用数学逻辑对命令式计算机程序的正确性进行陈述。 Hoare 与 Robert Floyd 之前的贡献有关，后者发布了一个类似的流程图系统。 与解释执行路径的弗洛伊德方法相反，霍尔总署使用源代码。

或者，也可以使用 wp 演算，与霍尔总编相反，其中进行了反向分析。

霍尔总编辑的核心元素是霍尔三元组，它描述了程序部分如何改变计算的状态：

{P}S{Q}。

P和 Q 是断言， S 是程序段。 P 是前置条件而 Q 是后置条件。 如果前置条件为真，则程序段执行后后置条件为真。 断言是谓词逻辑的公式。

三元组可以这样理解：如果 P 在执行 S 之前的程序状态成立，那么 Q  在执行之后成立。 如果 S不终止，那么就没有 after，所以在这种情况下 Q 可以是任何语句。 事实上，对于 Q，人们可能错误地选择了表达 S 不终止的陈述。 这称为部分正确性。 如果 S  总是终止，然后 Q 为真，我们就说完全正确。 终止必须独立证明。

霍尔总编辑包含公理和推导规则，适用于简单命令式编程语言的所有结构：

如果程序段 S不改变任何变量，断言也不改变，所以后置条件与前置条件相同：

{ P } S { P } {\displaystyle {\frac {}{\{P\}S\{P\}}}}

赋值公理指出，在赋值之后，每个语句都适用于先前为赋值右侧保留的变量：

{ P } x := E { P } 。

P  是将 P 中每个自由出现的 x替换为 E 的陈述。

严格来说，赋值公理不是单一公理，而是无限公理集的模式，因为 x  、 E 和 P 可以采用任何可能的形式，并且P可以由此构造。

如上所述，所描述的演算仅适用于证明部分正确性。 为了证明完全正确，while 规则必须通过循环变体进行扩展。 这是一个函数或变量 t {\displaystyle t} ，代表一个初始值为 z {\displaystyle z} 的数字。 现在必须证明 t {\displaystyle t} 在循环的每次迭代中都会减少，并且循环会在某个减少的值处终止。

使用霍尔总编辑和正式规范，可以检查程序或程序的某些部分的正确性。 因此，它提供了为数不多的可以实际证明正确性而不仅仅是确定错误存在的方法之一。但是，必须谨慎对待霍尔总编辑的分析结果：

• 如果规格不正确，分析结果可能是正确的，但与不正确的规格相比。
• 霍尔总编辑不会发现任何由编程语言本身的规范错误或错误的编译器引起的错误。
• 霍尔总编辑在大型软件系统中很快达到极限，尤其是在全局变量和递归的情况下。
• 必须使用计算机算法的公理来进行验证，这些公理考虑了整数类型可以表示的整数的局限性和浮点数的不精确性等特殊性。