霍尔逻辑（Hoare Logic）

霍尔逻辑是一种用于严格证明命令式程序正确性的形式化演绎系统，其核心记号是霍尔三元组，形式为在满足前置条件的状态下执行某段程序后，若程序终止则结果满足后置条件。

概述

霍尔逻辑由英国计算机科学家托尼·霍尔（Tony Hoare）于1969年提出，是公理语义的代表。它不描述程序如何执行，而是提供一组推理规则，让人们通过逻辑推导证明程序满足给定的规约，从而把程序验证转化为数学证明问题。

核心原理

• 霍尔三元组：由前置条件、程序、后置条件三部分组成，断言程序在前置条件成立时执行后建立后置条件。
• 赋值公理：证明赋值语句的关键规则，通过在后置条件中用表达式替换变量得到前置条件。
• 顺序规则：将两段程序的三元组通过中间断言拼接。
• 循环不变式：证明循环正确性的核心，是在每次迭代前后都保持成立的断言。
• 部分正确性与完全正确性：前者不保证终止，后者额外要求程序必定停机。

应用场景

霍尔逻辑是程序验证、形式化方法、静态分析的理论基础，被广泛用于关键软件的正确性证明。现代的分离逻辑正是它的扩展，用于处理指针与堆内存。许多验证工具和自动定理证明器背后都以霍尔逻辑为骨架。

常见问题

问：循环不变式为什么这么重要？答：循环可能执行任意多次，无法逐次展开证明，只有找到一个在每轮迭代都保持成立的断言，才能借助归纳一举证明整个循环的效果，因此循环不变式是循环验证的关键。

问：部分正确性和完全正确性有何差别？答：部分正确性只保证若程序终止则结果正确，不排除死循环；完全正确性则额外证明程序一定会终止，通常需要引入一个随迭代递减的度量。