Program Verification 04 - Weakest Precondition
# 前置知识
在阅读本文档前,请确保你已了解霍尔逻辑的相关概念,详见 Program Verification 知识板块中的 03 - Hoare Logic 文档。
# 前言
最弱前置条件由 Dijkstra 在 1975 年提出,在最初的出版物中并不是用霍尔逻辑描述的,而是以非形式化的方式介绍的。然而各大名校的课程均使用霍尔逻辑形式化地描述最弱前置条件,该方法确实清晰适用,因此本文也沿用这一方法。
# 先导概念
# 前置条件的强与弱
前置条件的强弱是一个容易混淆的概念,为便于理解,我们从一个实例入手对其进行介绍。考虑如下霍尔三元组:
不难发现,我们可以将前置条件 替换为 ,霍尔三元组仍然是合法的。在这里我们说前置条件 比 更 强 (strong) ,或者说 比 更 弱 (weak) 。
- 对于条件的“强”和“弱”可以这么理解:条件更强指的是对变量的取值范围有更强的约束。因为 ,即 ,所以 是更强的条件。
# 前置条件的强化和弱化
若 且 ,则显然有 。称该过程为对前置条件的 强化 (strengthen) 。回顾霍尔三元组的前置条件强化规则:
然而,若 且 ,我们不能简单地对前置条件进行 弱化 (weaken) 并替换得到 。事实上,当 成立时,我们就可以进行弱化。
- 因为 ,所以若 ,则 。
仍然是前面的例子,该三元组的前置条件可以替换为 、 、 ,但不能是 ,因为当 时 :
更一般地,对于某个霍尔三元组 ,令 ,我们可以想像一系列越来越弱的前置条件 ,其中 比 (严格)更弱,即 ()。
不难发现,尽管这样的序列可能是无穷长的,但是一定存在一个极限(至少可以是永真式 )。事实上,该极限即是对应于 和 的最弱前置条件。
# 术语
我们借助状态、大步操作语义和伪状态来描述不同初始状态下的最弱前置条件。
对于引入了 不确定性 (non-determinism) 的程序,从相同的状态出发执行相同的程序可能会有不同的执行路径,以及不同的结束状态。
在这种情况下,我们将记号 扩展为集合,例如 表示从状态 出发执行 可能会结束于状态 、也可能会结束于状态 、还可能不能正常终止。
- 若 是确定性程序或集合中仅含一个元素,则可能省略 ,例如 。
此外, 表示集合中的所有结束状态都满足谓词 。
# 基本概念
对于给定的程序 和后置条件 ,定义其 最弱前置条件 (weakest precondition) 为 ,满足:
。
。
对于前面的例子, 就是该霍尔三元组(在整数域上)的最弱前置条件。
- 前置条件的弱化必须保证霍尔三元组仍然成立,因此最弱前置条件是 ,而不是 甚至是 。
最弱前置条件是描述完全正确性的。作为对应的概念,最弱宽松前置条件是描述部分正确性的。
对于给定的程序 和后置条件 ,定义其 最弱宽松前置条件 (weakest liberal precondition) 为 ,满足:
。
。
对于给定的 和 ,最弱前置条件和最弱宽松前置条件都是唯一的(当然,可能有语义等价的不同逻辑公式)。
我们知道,完全正确性是终止性与部分正确性的结合,因此 和 之间必然有直接的关联,关键在于如何刻画程序 是否能正常终止 。
性质: 对于给定的初始状态 和程序 ,若 ,则 的执行能够正常终止。
证明
对于给定的 和 ,在不同的前置条件下,程序的执行结果可以被划分为三个不相交集,因此可以将对应的前置条件同样划分为三个不相交集:
执行 后到达的程序状态满足 。
执行 后到达的程序状态满足 。
执行 后程序不能正常终止。
由最弱前置条件的定义可知,第一个集合由 刻画,第二个集合由 刻画,因此第三个集合由 刻画,所以 表示程序能够正常终止。
因此 和 之间的关联 的形式化描述如下,其中 刻画了程序能够正常终止的性质:
另外,由上式可得:
需要注意的是, 不能说明 的执行不能正常终止。
注:事实上,对于完全正确性和部分正确性之间的关系,使用最弱前置条件和霍尔逻辑来描述在语义上是等价的,读者可以对照二者进行体会。
# 基本性质
性质: 对于任意的程序 和后置条件 ,有 。
性质: 对于任意的程序 和后置条件 ,有 。
性质: 对于任意的确定性程序 和后置条件 ,有 。
- 思考:为什么非确定性的程序不满足这个性质?
性质: 对于任意的程序 ,有 。该性质被称为 排奇律 。
证明
假设存在初始状态 和程序 ,使得 。
不妨从状态 出发执行 ,根据定义可知,此次执行能够正常终止,且终止时满足 ,而 是不可满足的,矛盾。
性质: 对于任意的程序 和后置条件 ,若 ,则 。该性质被称为 单调性 。
性质: 对于任意的程序 ,有 。这可以由 的定义直接得出。
性质: 对于任意的初始状态 和程序 ,若 ,则 的执行不能正常终止。
证明
由 和 之间的关联可知 ,而 。若 ,则必有 ,即 的执行不能正常终止。
对于任意的程序 ,有 。否则就会存在一个程序状态,既保证能终止、又保证不能终止。
性质: 对于任意的程序 和后置条件 ,有 。
证明
设 ,则 ,且程序能够正常终止,即 。由 和 的关系可知必有 。
性质: 对于任意的程序 和后置条件 ,有 。
证明
设 ,则 。
假设程序不能正常终止,即 ,而 。又对于 有 ,所以 。
性质: 对于任意的确定性程序 和后置条件 ,有 。
证明
设 ,则 ,所以 ,即 。
而对于非确定性程序 ,尽管 ,仍然有可能存在 使得 。所以 。
性质: 对于任意的初始状态 ,确定性程序 和后置条件 ,若 ,则 ,即程序不能正常终止。
证明
因为 ,所以 ,所以必有 。
而对于非确定性程序 ,尽管 ,仍然有可能存在 使得 。所以不能说明 。
# 初始状态空间划分
对于任意的(确定性或非确定性)程序 ,有:
若 ,则 。
若 ,则 。
若 ,则 。亦可写作:
对于任意的非确定性程序 ,有:
若 且 ,则:
若 且 ,则:
若 且 ,则:
若 且 ,则:
- 。
综上,我们可以仅用 将程序的初始状态空间划分为七个不相交集, 其中后四种情况仅在 为非确定性程序时存在:
[a] 执行 后的最终状态满足 。
[b] 执行 后的最终状态满足 。
[c] 执行 后不能正常终止 。
[ab] 执行 后能够正常终止,但不能确定最终状态是否满足 。
[ac] 如果执行 后能够正常终止,那么最终状态就满足 ,但不能确定是否能终止 。
[bc] 如果执行 后能够正常终止,那么最终状态就满足 ,但不能确定是否能终止 。
[abc] 执行 后不确定是否能终止,也不确定如果终止是否能满足 。
- 01
- Reading Papers - Kernel Concurrency06-01
- 02
- Linux Kernel - Source Code Overview05-01
- 03
- Linux Kernel - Per-CPU Storage05-01