形式化方法--程序的正确性验证-14.doc

第十四讲形式化方法--程序的正确性验证
一、概述
计算机的程序是一种静态的对象,但它所描述的问题(问题的解)却是一个动态的对象。所谓的程序设计就是用程序设计语言中的语句改变程序中数据对象的状态,构造所描述问题的动态行为。这是不自然的,程序所描述的动态行为也无法直接用程序本身的静态结构进行正确性证明。
形式化规约(formal specification)是需求阶段的形式化说明,是用户需求的严格描述,其一般形式用Hoare逻辑描述[1]如下:
├{Φ}P{Ψ} <1>
其中Φ和Ψ分别表示初始和结束断言条件,其含义是:“假如初始状态dI满足条件Φ,那么程序结束并且终结状态df必须满足Ψ”。
设D=D1×……×Dn为程序P的状态空间,其中,Dj(j=1,……,n)表示程序中数据对象的值域。显然,由Φ和Ψ断言条件所确定的合法初始和结束状态的集合是D的一个子集。
执行函数E:Φ×P→Ψ定义如下:
无定义对合法的初始状态di,程序P不结束
E(P,dI)=
终结状态df 对合法的初始状态di,程序P结束
程序的正确性即为:
├{Φ}P{Ψ}
iff <2>
"di(├Φ(di)→(├程序P结束 and ├Ψ(E(P,di))))
总地来讲,验证一个程序的正确与否有两种办法,一种是程序的测试,另一种是程序的正确性证明。
程序的测试与程序的验证
对给定的一个合法的初始状态di,当程序执行结束时其终结状态为df,那么,Φ(di)和Ψ(df)都应该被满足。这一点可用下式表示:
{di}P{df} <3>
所谓程序的测试就是验证测试用例{di}P{df},即验证程序对di的执行结果是否为df。由于合理的初始状态是无限的,因此,对程序验证来讲,测试不是一个完备的方法。测试被认为是一种尽量发现错误,但并不能保证程序中没有错误[2]的方法。对大数应用来讲,它是可满足的;但对有些应用来讲,测试是一种不能满足的验证方法,例如:航空、航天等领域的软件系统。
显然,对要求绝对正确的软件,测试是一种不能采用的方法。无论白盒测试还是黑盒测试都是在无限集合{(di,df)|"di,"df, di和df满足{di}P{df}中选择有限的一些(di,df)对进行验证,而各种测试方法只是选择(di,df)的策略不同而已。
因此,验证程序是否完全正确要寻求另外的解决途径。那就是程序的正确性验证。
形式语义与程序的正确性验证
程序的正确性验证应该具有严密的推量过程,以保证程序每步执行结果都是希望的结果,而与程序执行的某个初始状态无关。程序的正确性证明现有三种方式:操作语义、指称语义和公理语义。它们分别用不同的形式化方法,严格地证明一个程序是否正确。尽管这种方法还不够完善,还不为一般软件人员所掌握,但它确实是保证软件绝对正确的唯一途径。
操作语义(Operational Semantics)
操作语义的根据是,一种程序设计语言一但在某种计算机系统中实施,其语义的含义也就完全确定下来了,因此,自然地就用语言的实施作为语言含义的定义,故称这种语义为操作语义。
当然,这种实施应该在一种标准的、抽象的机器上进行。,称为“栈-环境-控制-外存”。IBM公司提出了一种可描述程序设计语言语义的元语言:VDL。后来,英国的爱丁堡大学提出了更一般的方法:在数据结构上用数学关系建立操作语义的解释系统。
这种方法的本质就是,用抽象机器的状态空间和最简单的基本指令来定义抽象语言的语义,将抽象语言的程序转换为一系列抽象机器的基本指令序列。这种对应关是固定的,而且抽象机器的基本指令的含义是固定的,这样一个程序设计语言的程序就有了一个明确的、无二义的语义。
为了验证一个抽象程序的正确性,就必须在抽象计算机上执行其相应的基本指令序列。基本指令序列的一次执行只能验证一组输入、输出状态之间的关系。因此,用操作语义验证一个程序的正确性实质上是一种测试型的验证方式。
指称语义(Denotational Semantics)
指称语义学认为,程序设计语言的语义是由其语言成份的语义决定的,而程序设计语言成份的语义应该是其本身固有的,与程序设计语言的个体实现无关。指称语义的出发点是语言成份执行的最终结果,而不是其执行过程。这种执行结果是由语言成份形式后面隐藏的所指物决定的,故这种方式也称为指称语义。
,,故指称语义也称为牛津语义。IBM公司也创立了基于指称语义的VDM软件开发方法。
指称语义的指称物均为数学对象,如整数、集合和映射等。指称物的集合称为论域。一个语言的指称语义就是确定该语言的相关论域,并给出语法成份到论