指称语义
已经学习了两种操作语义,这一节,我们学习新的语义模型–指称语义。指称语义意用数学函数表达程序在计算什么,以IMP为例子就是一个把store转换为另一个store的函数:给定一个store,程序输出一个最终的store。举个例子,可以把程序
IMP的指称语义
给定程序c,我们用
其中
现在我们能定义IMP的的指称语义了。首先定义算术表达式的布尔表达式的指称:
命令的指称如下:
定义关系运算
如果
但是只要你仔细一看,就会发现while的定义是不对的,它在自己的定义中用到了自己,这就不是一个定义了,而是一个递归等式,解决这个问题的方法就是不动点。
不动点(Fixed points)
为了解决while定义的问题,我们必须找出符合递归等式的函数。为了理解这个问题,我们先理解下面这个例子,给定函数
这不是
利用逐步渐近法,我们可以计算出不动点。每次计算就越来越逼近最终的答案。为了求出满足递归等式的
但是数学中没有‘显然’,接下来就是给逐步渐进法建立一个数学模型:一个高阶函数F,F接受一个
其中
上述等式的一个解就是
Kleene不动点定理与IMP
让我们利用不动点重新定义IMP的while语义:
但是认真的读者肯定心中已经有个疑问了:“你怎么确定不动点存在?”,是的,就像上一节所说的那样,递归等式不一定有解,不动点不一定存在。这一节就要利用Kleen不动点定理证明while命令的语义是存在不动点的。
Kleene不动点定理
proof. 如要证明A=B,可以先证明
- Case
:因为 ,根据单调性可得 ,又因为对所有 , 都满足 ,所以 。Case finished; - Case
:假设左边的 的结果是b,根据上面的解释,其实只需要输入的有限子集 就能输出b, ,所以 ,假设有一个比 稍微大一点的z,根据单调性有 ,所以有 ,根据有向集合的定义,有 ,所以 。Case finished,得证。
proof. 设
然后,我们证明
所以所有元素的并集
指称语义的论证
相比操作语义,指称语义的一大好处就是,在论证等价问题的时候,只需要看程序指称的计算结果就行了,而操作语义则必须把抽象机器底层变换、衍生出的都论证清楚。
比如,要证明
利用偏函数,映射关系和集合,证明变得容易多了。再举个例子
由Kleene不动点定理可得
公理语义
什么是公理语义
公理语义用逻辑规则来定义程序(操作语义模型展示程序如何运行,指称语义模型展示程序计算什么)。公理语义最初由Floyd和Hoare提出,后来由Dijkstra和Gries进一步发展。
公理语义通常用前置条件和后置条件来描述程序规则:
其中c是程序,Pre和Post是描述程序状态的公式,通常称之为断言;这种三元逻辑又称之为部分正确规则,或者霍尔三元组,其意思如下:如果在运行c前Pre成立,而且c是能终止的,那么Post在c终止后也成立。也可以这样说,给定满足Pre的store
前置条件和后置条件可以看成程序和用户的接口、约定,用户只需关系程序运行的结果,而不用理解程序是怎么运行的。通常,为了使程序更好维护,程序员用写注释的方法给方法、函数添加文档,特别是对那些闭源的库来说,这就是库使用者和库开发者之间的约定。
但是,谁也不能保证写在注释里的前置条件和后置条件是正确的,注释描述的是开发者的意图,而不能保证程序的正确性。公理语义解决的就是这个问题。
公理语义展示了如何描述部分正确语句以及用论证证明程序的程序性。但是,部分正确规则不能保证程序会终止,这也是它叫‘部分’的原因,而完全正确规则保证了程序在满足前置条件时一定会终止,我们用方括号表示完全正确规则:
其意思:如果在执行c之前满足Pre,那么c会终止并且终止后满足Post。
大体上,在霍尔三元组中,前置条件指明了在运行程序前的需求,后置条件指明了程序的期望结果(如果程序会终止)。举个例子:
表明了如果有个store中有foo和bar,分别映射到0和i,那么如果程序终止,那么最终的store中应该包含baz到-2i的映射。注意其中i只是个逻辑需要的变量,程序中并没有i,它的作用只是表述bar的初始值,通常称这种变量为‘伪变量’(ghost variables)。
例子中的部分正确语句是正确的:给定任何满足
则
表明了如果有个包含foo到0、bar到正整数映射的store
我们所讲的公理语义会主要集中在部分正确断言。
断言
- 怎么写断言?怎么描述前置条件和后置条件?
- 一个断言合理是什么意思?一个部分正确语句合理是什么意思?
- 怎么证明部分正确语句是合理的?
怎么表述前置条件或者后置条件?上面的例子中,我们已经用过了程序变量、逻辑相等、逻辑变量、逻辑合取(
为了表示什么是“断言P在store
接着定义方法
现在我们能表示断言的正确性了,
定义了断言的正确性,现在我们就可以定义一个部分正确语句的正确性了:
当一个霍尔三元组是合理的(写作
现在我们知道当我们说断言P成立、部分正确语句
霍尔逻辑
利用公理和推论,我们可以直接推导出合理的部分正确语句,而不用关心store或者程序,这些就叫做霍尔规则,由霍尔规则组成的证明系统就是霍尔逻辑:
while中的断言
这些霍尔逻辑组成了部分正确语句的归纳定义。当我们能为
soundness和completeness
现在我们已经有两种断言:
- 合理的部分正确语句
。其在所有的store和解释中都成立。 - 霍尔逻辑公理
。能从霍尔逻辑的公理和推论中推导出的部分正确语句。
这两者之间有什么关系呢?首先,第一个问题,是不是每个霍尔逻辑公理都是合理的部分正确三元组呢(
第二个问题,对每个合理的断言,我们都能构造出一个霍尔逻辑吗(
例子:阶乘
{x=n ∧ n>0}
y:=1;
while x>0 do {
y:=y*x;
x:=x-1;
}
{y=n!}
我们会用霍尔逻辑证明上面是计算n的阶乘的程序。
要证明上面的程序,因为这是一个包含一个赋值语句和一个while语句的程序,就要利用SEQ规则,于是我们要证明下面的两个三元组:
但要想利用SEQ规则,要先满足SEQ规则的分子(前提条件),也就是要先找到满足上面两个三元组的
两边同时乘x!,得到x!*y=n!,当然其中的x是正整数。于是我们得到
要证明
要证明上式,我们倒着走一遍:
又因为
剩下的只需证明
由CONSEQUENCE规则可得第二个三元组。
下面,证前一个三元组。首先,利用不需要前提条件的赋值规则:
又因为
小结
到这里就告一段落了,写了不少,基本介绍了语义,以及证明语义属性的方法。