8.Hoare的公理化方法

8. Hoare的公理化方法该方法的主要思想是给出公理系统，包含赋值公理规则、复合推理规则、条件推理规则、循环推理规则和推论规则。

8.1 Hoare逻辑和Hoare演算定义8.1 （Hoare逻辑的语法）令B是谓词逻辑的基，B上的Hoare公式是形如{p}S{q}的表达式，其中p, q∈WFF B是谓词逻辑里的公式，S∈L2B是一个循环程序。

基B上的Hoare公式全体记为HF B。

定义8.2 （Hoare逻辑的语义）给定谓词逻辑的基B，令I是B的一个解释，∑是相应的状态集合。

每个Hoare公式{p}S{q}∈HF B都被一语义范函，亦记为I，映射成一个函数：I({p}S{q}):∑→Bool，此函数定义为：对于σ∈∑，I({p}S{q})(σ)=true当且仅当若I(p)(σ)=true且M I(S)(σ)有定义，则有I(q)(M I(S)(σ))=true。

RMK.（1）每当I(p)(σ)为假或M I(S)(σ)没定义，I({p}S{q})(σ)就为真。

这就是说，“Hoare公式{p}S{q}在某解释下恒真”恰恰就是说“S关于公式p和q是部分正确的”。

（2）程序的含义M I(S)有操作语义和指称语义之分。

与谓词逻辑类似，有以下符号记法：⊨{p} S {q} “Hoare公式在解释I下恒真”I⊨{p} S {q} “Hoare公式在解释I下逻辑恒真”W⊨{p} S {q} “Hoare公式是公式集合W⊆WFF B的逻辑结果”例8.3（1）在通常的解释I下，Hoare公式{x>5} x:=2*x {x>20}成真的条件是什么？对于某状态σ，I({x>5} x:=2*x {x>20})(σ)=trueiff I({x>5}(σ)=false，或I({x>20}(M I( x:=2*x)(σ))=trueiff σ(x)≤5，或M I( x:=2*x)(σ)(x)>20iff σ(x)≤5，或(σ)(x) > 10（2）证明：在通常的解释I下，⊨I{true}while x≠10 do x:=x+1 od {x=10}。

令while x≠10 do x:=x+1 od是循环程序S。

根据Hoare公式的语义定义，只需证得：对于任意状态σ，或M I(S)(σ)没定义，或I({p}S{q})(σ)为真，就足够了。

显然要么σ(x)≤ 10，要么σ(x)>10。

若σ(x)>10则M I(S)(σ)没定义；若σ(x)≤ 10则M I(S)(σ)(x)=10。

（3）证明：{y+1>y}⊨{true}x:=y+1{x>y}对于任意解释I和任意状态σ，I(x>y)(M I( x:=y+1)(σ))=trueiff I(x>y)(σ[ x/I(y+1)(σ)])=trueiff I(y+1>y)(σ)=true （根据代入定理）iff I是{y+1>y}的模型。

8.1.1 Hoare演算我们知道，演算的含义就是从已知的恒真公式（如公理）推出更多的结论（如定理）。

一、赋值公理现在要研究的是形如{p}x:=t{q}的Hoare公式，具体要研究其中的公式p和q之间有何关系？赋值公理就是给出它们之间的具体关系．．．．．．．．．．．．．．．．．。

作为例子我们来考虑{x>0}x:=x+1{x>1}。

为了便于讨论，不妨把变量x 的旧值（执行前）表示为x，把新值表示为x'。

现在可把本例的Hoare 公式视为如下公式：x>0∧ x' =x+1⊃ x'>1注意，该逻辑式由三部分组成，其一是前置条件x>0，其二是变量的新老值间的关系式，其三是后置条件x'>1，并且前置条件只含老值x，而后置条件只含新值x'。

新旧关系式中即包含新值也包含旧值。

从上述分析不难看到，如果从新老值的关系式求出新值，并将它代入．．．．．．．．．．．．．．．．．．．．到后置条件里，．．．．．．．x+1>1，则会得到只由老值组成的前置条件；同样，如果从新老值的关系式中求出老值，并将它代入到前置条件中．．．．．．．．．．．．．．．．．．．．．．．．．．．，x'-1>0，则会得到只由新值组成的后置条件式。

这就是从前置条件求后置条件和从后置条件求前置条件的问题。

这里的一个关键问题是，如何从新老值的等式求出新值或老值。

显然，求新值是非常简单的事情，因此，从后置条件求前置条件是较容易的．．．．．．．．．．．．．．．事情．．；但想从前置条件求后置条件，有时并不那么容易，因为．．．．．．．．．．．．．．．．．．．．．．．．这时需要通过求反函数的方法来求老值。

如果反函数是容易求到的，那么从前置条件求后置条件也变成容易的事情。

据上述讨论，我们不难理解所给出的下面赋值公理。

这条公理正是采用了从后置条件求前置条件的思路。

考虑下面几个验证公式:1) {x=0}x:=x+1{x=1}2) {x >0}x:=x+1{x >1}3) {x >0}x:=x+1{x >0}4) {x >0}y:=x+1{x >0∧y >1}它们都是恒真的Hoare 公式，即前面均可带上“⊨”。

但它们并不都可从赋值公理直接导出（其中的公式3）不能从赋值公理直接导出）。

二、 复合语句规则考虑形如{p}S 1; S 2{q}的验证公式。

显然，如果存在某个r ，使公式{p}S 1 {r}和{r}S 2{q}成立，则在S 1的入口处p 的成立，能保证在S 2的出口处q 的成立。

故复合语句的规则可如下： （i ） 赋值公理 {p x t } x:=t {p} 对于所有p ∈WFF B ，x ∈V ，t ∈T B 。

（ii）复合语句规则{p}S1{r}, {r}S2{q} 对于所有p,q,r∈WFF B, S1,S2∈L2B{p} S1 ; S2{q}三、条件语句规则考虑形如{p}if e then S1 else S2 fi {q}的Hoare公式。

条件语句将产生一条相应的推理规则，称之为条件规则。

从条件语句的入口到出口的路有两条，一是条件表达式e为真的路，一是e为假的路。

经过这两条路的条件分别为p∧e和p∧⌝e。

故如果有：p∧e⊃q和p∧⌝e⊃q则在出口处q自然成立。

（iii）条件语句规则{p∧e}S1{q}, {p∧⌝e}S2{q} 对于所有p,q∈WFF B, e∈QFF B, S1,S2∈L2B{p} if e then S1 else S2 fi{q}四、循环语句规则最后考虑循环语句的规则。

假设有循环语句while e do S od，令当前状态为σ，则循环的执行过程是：（用σ）计算e的值；检查它是否为真？若为真则执行S并重复执行上述过程；若为假，则循环将终止。

由此可知在循环的出口处条件⌝e一定满足，即它是后置条件中的一部分。

另外我们还能注意到，如果有一断言p 满足“在执行循环体之前p 成立，则执行S 后p 仍然成立”，即有性质{p ∧e} S {p}，则在循环的出口处p 也成立。

根据上述讨论，可给出下面所示的循环语句规则。

五、 推论规则假设已知公式{p} S {q}成立，并且有q ⊃ q '， p ' ⊃ p ，即可以强化前置条件，或可以弱化后置条件，则新的公式{p '} S {q '}更应该成立。

于是可给出下面所示的一条推论规则。

（iv ） 循环语句规则 {p ∧e} S {p} 对于所有p ∈WFF B , e ∈QFF B , S ∈L 2B {p} while e do S od {p ∧⌝e} p ∧e （v ） 推论规则 p ' ⊃ p, {p} S {q}, q ⊃ q ' 对于所有p, q, p ' , q '∈WFF B , S ∈L 2B {p '} S {q '}派生规则（derived rule ）:若存在从谓词逻辑所有的逻辑恒真公式和{s 1, …, s n }到s 的一个演绎，则称是一条s s s n ,...,1派生规则。

定义 （循环不变式）设while e do S od 是循环语句，e ∈QFF B ，且有⊨{r ∧e} S {r}则称r 为该循环语句的不变式（invariant ）。

（I ） 对于所有p, q ∈WFF B ，x ∈V ，t ∈T B ， p ⊃q x t {p} x:=t {q} （II ） 对于所有p 0, …, p n ∈WFF B , S 1, …, S n ∈L 2B (n ≥2) {p 0} S 1 {p 1}, {p 1} S 2 {p 2}, …, {p n-1} S n {p n } {p 0} S 1; …; S n {p n } （III ） 对于所有p, q, r ∈WFF B , e ∈QFF B , S ∈L 2B p ⊃ r, {r ∧e} S {r}, (r ∧⌝e)⊃ q {p} while e do S od {q}定理（循环不变式的合取式也是一个循环不变式）若r和r'是while e do S od的循环不变式，则r∧r'是循环不变式。

证明：只需证明⊨{r∧r'∧e} S {r∧r'}。

（这是比较直观的问题，但又不是显然的问题，这需要证明，因为在强化前置条件的同时强化了后置条件）。

具体证明：任一不等于ω的σ都使下式成立：I(r∧r'∧e)σ⊃ I(r∧r')(M I(S)(σ))RMK.这里要注意的有两点：一是循环不变式并不保证执行循环体之前一定．．．．．．．．．．．．．．．．．．成立．．，它只保证“如果在执行循环体之前成立，则执行后也成立”。

二是循环不变式可有无穷多个。

当证明程序时需要找够证明程序正确性的合适的循环不变式，当然不一定唯一。

定义（合适循环不变式）设r是循环语句while e do S od的一个循环不变式。

如若还满足条件p⊃ r和r∧⌝e⊃ q，则称r为公式{p} while e do S od {q}的合适循环不变式。

RMK.其中第一条表示入口处若p成立，则r也成立；第二条表示r要强到r∧⌝e能蕴含q的程度。

定义（Hoare公理系统）由以上赋值公理、复合推理规则、条件推理规则、循环推理规则和推论规则所组成的公理系统称之为Hoare公理系统。

8.2 可靠性与相对完备性定理8.5 （可靠性，soundness）令B是谓词逻辑的基。

对于任意公式集W⊆WFF B和HF B中的任意公式{p} S {q}（满足p, q∈WFF B和S∈L2B），若W⊢{p} S {q}，则有W|={p} S {q}。