高完整性系统——霍尔逻辑

阅读：评论：0

高完整性系统——霍尔逻辑

霍尔三元组

同样的方式：当 x=1 作为 postcondition holds 的时候，precondition 我们也很容易推出就是 x=0
但是这里的 precondition 被是 weakest precondition
这是因为，我们反向推理（backwards) 的难度低于正向推理 (forward)
还有一种理解方法就是：
x > 5 = > x > 3 x>5 => x>3 x>5=>x>3 因此我们说 x > 5 x>5 x>5 是更加严格的条件；也就是更加 strong 的条件。同样的我们来看这个 post condition
如果我们能够通过 precondition 得到 x=3 我们可以根据 x=3 这个条件推导出其他更加宽松的 postcondition，比如 x > 2 x>2 x>2，此时我们的式子可以写成这样：
{ x = 2 } x : = x + 1 { x > 2 } {x=2} x:=x+1 {x>2} {x=2}x:=x+1{x>2}
这是完全没有问题的，而 x > 2 x>2 x>2 的条件是不如 x = 3 x=3 x=3 strong 的
同样的道理我们看为什么是 weakest precondition：因为当我们用一个比现在 precondition 更严格一点的条件，这个推导式子也同样成立：
x + 1 = 3 = > x = 2 x+1=3 => x=2 x+1=3=>x=2
所以我们认为 x + 1 = 3 x+1=3 x+1=3 这个条件比 x = 2 x=2 x=2 严格，于是我们带到原式子中：
{ x + 1 = 3 } x : = x + 1 { x = 3 } {x+1=3} x:=x+1 {x=3} {x+1=3}x:=x+1{x=3}
这个式子当然也是成立的

我们可以从 post 的结果很容易推出 pre 的结果
尤其是第二个式子，我们只需要根据结果x=1 和条件 x:=x+1 甚至不需要计算出来 x=0 我们只需要把 x:=x+1 的过程反过来就可以退出 pre
同样的：
对于这个式子，我们也可以轻易的写出
再看前面 forward 推理很难的那个问题
这里我们只需要
有上面的现象我们可以得到 rule of assignment

P P P 是关于 x x x 的公式，经过将 x:=E 这个过程之后 P P P holds，
那么我们把 post condition 中的 x 全部用 E 来代替即可
这个式子中 E = x + 1 E=x+1 E=x+1 所以把 post condition 中的 x = 1 x=1 x=1 中的所有 x x x 替换成 E E E 作为 precondition 即 x + 1 = 1 x+1=1 x+1=1
所以结果就是:
{ x + 1 = 1 } x : = x + 1 { x = 1 } {x+1=1} x:=x+1{x=1} {x+1=1}x:=x+1{x=1}
{ x = 0 } x : = x + 1 { x = 1 } {x=0}x:=x+1{x=1} {x=0}x:=x+1{x=1}
再练一个：

根据我们前面讨论的 forward 和 backward 我们可以通过这个公式推导出：
如果我们满足了下面的这种情况，我们同样能够得到
因为 x = 0 x=0 x=0 的条件比 x > = 0 x>=0 x>=0 要严格，因此作为 precondition 也是可行的
由此
解析一下： P ′ P' P′ 是 P P P 的子集，同样的 Q Q Q 是 Q ′ Q' Q′ 的子集，因此 P P P 的范围要收窄，而 Q Q Q 的范围要扩大。

假设我们要证明：
首先我们先把这个式子作为 consequence rule 的下半部分，那么也就是 P ′ = { x = 0 } P'={x=0} P′={x=0}, Q ′ = { x > 0 } Q'={x>0} Q′={x>0}
我们接下来不改变 post condition，当我们想使用 consequence rule 的时候我们需要找到 P ′ = > P P'=>P P′=>P ，而我们现在有 P ′ = { x = 0 } P' = {x=0} P′={x=0}
所以公式变成了下述：
假设有一个中间变量 P P P 是被推导出来的
接下来对下图中的红框中的部分使用 assignement axiom
{ ? P } x : = x + 1 { x > 0 } {?P} x:=x+1 {x>0} {?P}x:=x+1{x>0} 可以推导出 P = x + 1 > 0 P=x+1>0 P=x+1>0
然后将这个带换到 x = 0 = > ? P x=0 => ?P x=0=>?P 的部分，就可以得到：
证明完成
总结以下上面的证明逻辑

证明这一类题目的时候我们通常还是从后面一个部分开始，backward 的方式进行证明
- 证明开始：
首先利用 rule of consequence 把 S 1 ; S 2 S1; S2 S1;S2 看成一个整体，此时 P ′ = { x = 0 } , Q ′ = { X = 2 } P'= {x=0}, Q'={X=2} P′={x=0},Q′={X=2}所以这个时候我们还是需要看 P ′ = > P P'=>P P′=>P 所以我们还是假设有一个中间的变量 ? P ?P ?P
现在还不能对对下图中框选的部分进行 assign rule，因为 assignment rule 只能对 single 的步骤进行，因此我们现在要对下图中框选的部分进行 rule of sequencing

并得到：
我们引入了一个中间变量 ? R ?R ?R，同时将中间推理拆分成两个 individual 的部分
这个时候，请注意下图中框选的部分：
这里有两个未知的部分 ? P , ? R ?P, ?R ?P,?R 因此，我们要寻求别的突破口，其实也非常明显，我们可以从最后的那个式子的 ? R ?R ?R 开始使用 assignment rule
当这个证明出来之后，顺理成章对左上角包含 ? P ?P ?P 的式子再使用 assignment rule 就可以了
现在只剩下最左边的一部分了：
事实上他是恒成立的：