Program Verification 03 - Hoare Logic
# 前置知识
在阅读本文档前,请确保你已了解操作语义的相关概念,详见 Program Verification 知识板块中的 02 - Operational Semantics 文档。
# 基本概念
霍尔逻辑 (Hoare logic, or Floyd–Hoare logic) 是一种形式化系统,用于严格推理计算机程序的正确性。
霍尔三元组 (hoare triple) 是霍尔逻辑的核心,其基本形式为 ,其中 和 分别为 前置条件 (pre-condition) 和 后置条件 (post-condition) , 是一个程序片段(即一系列的程序指令)。
- 前置条件和后置条件是用一阶逻辑公式描述的 assertion 。
非形式化地讲,霍尔三元组 合法 (valid) 的含义是:假定前置条件 成立,那么在执行完程序 之后,后置条件 将会成立。
可以从程序状态的角度描述霍尔三元组:从满足前置条件 的程序状态出发,执行程序 之后,到达的程序状态应当满足后置条件 。
- 如果从不满足 的状态出发,则执行 之后的结果是没有保证的,霍尔三元组并不生效,这和不合法是不同的概念。
如下是一些合法的霍尔三元组的示例:
在霍尔三元组中,仅用于前置和后置条件中、且具有恒定值的变量被称为 逻辑变量 (logical variables) 或 幽灵变量 (ghost variables) 。例如在下面的霍尔三元组中, 和 就是逻辑变量:
我们沿用在命题逻辑和谓词逻辑中使用的术语,用 表示状态,用 表示满足,例如 。特别地,用 表示霍尔三元组合法。
# 正确性
事实上,使用标准的霍尔逻辑只能证明 部分正确性 (partial correctness) ,因为它并不要求程序 能终止,例如下面的霍尔三元组也被视为是合法的:
非形式化地讲,完全正确性 (total correctness) 是终止性与部分正确性的结合。我们用不同的记号 来表示用于描述完全正确性的霍尔三元组,有时也用 表示。现在我们重新定义霍尔三元组的合法性:
一个描述部分正确性的霍尔三元组 是合法的,当且仅当:
从满足前置条件 的程序状态出发,执行程序 ;
如果程序 能终止,则执行指令之后到达的程序状态应当满足后置条件 。
一个描述完全正确性的霍尔三元组 是合法的,当且仅当:
从满足前置条件 的程序状态出发,执行程序 ;
程序 能终止;
执行指令之后到达的程序状态满足后置条件 。
形式化地讲:
如下是一些不合法的霍尔三元组的示例:
另外一些简单的特殊示例如下:
:如果 能终止,则 执行后 成立。
: 总是能终止且到达满足 的状态。
:该式对任意的 和 恒成立。
:如果初始时 成立,则 能终止。
# Tips
使用霍尔逻辑为程序设计 specification 并不容易。例如,假设我们希望形式化地描述“执行程序 能将 赋值为 ”,不熟练者可能会写出如下的霍尔三元组:
然而这样的后置条件会将很多事实上并不满足要求的程序证明为正确的,例如:
事实上,后置条件 描述的是“在执行程序 之后 的值等于 ”。如下为一种能够满足要求的形式化描述:
由此可见,使用霍尔逻辑进行程序验证是 non-trivial 的任务,形式化系统本身并不能保证程序验证的正确性。
# 基本推理规则
# 逻辑推理规则
合取和析取规则如下所示:
前置条件强化 (strengthening precedent) 的规则如下所示:
后置条件弱化 (weakening consequent) 的规则如下所示:
在这里,读者可能对“强”和“弱”的描述有些困惑,有关前置条件强弱的更多内容详见后文。
# 语句推理规则
skip 语句的推理规则如下所示:
赋值语句的推理规则如下所示,这是一种看似反直觉的后向风格的描述:
如下是看似等价的前向的描述,然而这是错误的,例如 就无法用该规则正确地推理:
顺序语句的推理规则如下所示:
条件语句的推理规则如下所示:
# 循环推理规则
# 终止性规则
我们知道,完全正确性是终止性与部分正确性的结合,而除去运行时错误,只有循环语句可能会导致程序不能正常终止。因此只有循环的推理规则是不同的,这也是将完全正确性和部分正确性区分开来的核心规则。
事实上,完全正确性和部分正确性的关联也可以表示为推理规则:
此外,令 表示 中不含 while 语句,则还有下列规则:
# 循环不变式
循环不变式 (loop invariant) 是满足如下条件的逻辑表达式:
在开始执行循环之前该式为真;
如果在某次迭代之前该式为真,那么在下次迭代之前该式仍然为真;
在循环终止时该式为真,并且该式应该告诉我们一些有用的、能帮助我们理解程序语义的信息。
对于某个循环语句,可能存在多种不同的循环不变式。
循环不变式是用于程序测试和验证的概念。
# 部分正确性的推理规则
while 语句的描述部分正确性的推理规则如下所示,其中 是循环不变式:
为什么是 ?可能执行多次 才破坏 ?
# 完全正确性的推理规则
while 语句的描述完全正确性的推理规则如下所示,其中 是循环不变式, 是逻辑变量(即不会出现在 中), 是循环计数器:
具体地讲:
霍尔三元组 描述了循环计数器 随迭代而递进的事实。
谓词逻辑 描述了循环在计数器超限后终止的事实。
- 01
- Reading Papers - Kernel Concurrency06-01
- 02
- Linux Kernel - Source Code Overview05-01
- 03
- Linux Kernel - Per-CPU Storage05-01