8.Hoare的公理化方法

程序理论第八章 第 1 页 共 12 页 1

8. Hoare的公理化方法

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

8.1 Hoare逻辑和Hoare演算 定义8.1 （Hoare逻辑的语法）

令B是谓词逻辑的基，B上的Hoare公式是形如{p}S{q}的表达式，其中p, q?WFFB是谓词逻辑里的公式，S?L2B是一个循环程序。 基B上的Hoare公式全体记为HFB。

定义8.2 （Hoare逻辑的语义）

给定谓词逻辑的基B，令I是B的一个解释，?是相应的状态集合。每个Hoare公式{p}S{q}?HFB都被一语义范函，亦记为I，映射成一个函数：I({p}S{q}):??Bool，此函数定义为：对于???， I({p}S{q})(?)=true 当且仅当

若I(p)(?)=true且MI(S)(?)有定义，则有I(q)(MI(S)(?))=true。

RMK.

（1） 每当I(p)(?)为假或MI(S)(?)没定义，I({p}S{q})(?)就为真。这就

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

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

程序理论第八章 第 2 页 共 12 页 2

与谓词逻辑类似，有以下符号记法： ?I {p} S {q} “Hoare公式在解释I下恒真” ? {p} S {q} “Hoare公式在解释I下逻辑恒真”

W?{p} S {q} “Hoare公式是公式集合W?WFFB的逻辑结果” 例8.3

（1） 在通常的解释I下，Hoare公式{x?5} x:=2*x {x?20}成真的条件

是什么？

对于某状态?，I({x?5} x:=2*x {x?20})(?)=true iff I({x?5}(?)=false，或I({x?20}(MI( x:=2*x)(?))=true iff ?(x)?5，或MI( x:=2*x)(?)(x)?20 iff ?(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公式的语义定义，只需证得：对于任意状态?，或MI(S)(?)没定义，或I({p}S{q})(?)为真，就足够了。显然要么?(x)? 10，要么?(x)?10。若?(x)?10则MI(S)(?)没定义；若?(x)? 10则MI(S)(?)(x)=10。 （3） 证明：{y+1?y}?{true}x:=y+1{x?y}

对于任意解释I和任意状态?， I(x?y)(MI( x:=y+1)(?))=true iff I(x?y)(?[ x/I(y+1)(?)])=true

iff I(y+1?y)(?)=true （根据代入定理）iff I是{y+1?y}的模型。

程序理论第八章 第 3 页 共 12 页 3

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，则会得到只由新值组成的后置条件式。这就是从前置条件求后置条件和从后置条件求前置条件的问题。

这里的一个关键问题是，如何从新老值的等式求出新值或老值。显然，求新值是非常简单的事情，因此，从后置条件求前置条件是较容易的．．．．．．．．．．．．．．．

程序理论第八章 第 4 页 共 12 页 4

事情；但想从前置条件求后置条件，有时并不那么容易，因为这时需．．．．．．．．．．．．．．．．．．．．．．．．．．要通过求反函数的方法来求老值。如果反函数是容易求到的，那么从前置条件求后置条件也变成容易的事情。据上述讨论，我们不难理解所给出的下面赋值公理。

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

考虑下面几个验证公式: 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}S1; S2{q}的验证公式。显然，如果存在某个r，使公式{p}S1 {r}和{r}S2{q}成立，则在S1的入口处p的成立，能保证在S2的出口处q的成立。故复合语句的规则可如下：

（i） 赋值公理

{pxt} x:=t {p} 对于所有p?WFFB，x?V，t?TB。

程序理论第八章 第 5 页 共 12 页 5

（ii） 复合语句规则

{p}S1{r}, {r}S2{q} 对于所有p,q,r?WFFB, 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自然成立。

四、 循环语句规则

最后考虑循环语句的规则。假设有循环语句while e do S od，令当前状态为?，则循环的执行过程是：（用?）计算e的值；检查它是否为真？若为真则执行S并重复执行上述过程；若为假，则循环将终止。由此可知在循环的出口处条件?e一定满足，即它是后置条件中的一

（iii） 条件语句规则

{p?e}S1{q}, {p??e}S2{q} 对于所有p,q?WFFB, e?QFFB, S1,S2?L2B {p} if e then S1 else S2 fi{q}

本文来源：https://www.bwwdw.com/article/4qlf.html