资源描述：
《程序正确性证明及循环不变式的寻找方法.pdf》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。
1、第D1O2I卷:10第.16436期8/j.cnki.issn1004-0366.2000.03.0甘11肃科学学报Vol.12No.32000年9月JournalofGansuSciencesSep.2000文章编号:1004-0366(2000)03-0043-06程序正确性证明及循环不变式的寻找方法王彩芬(西北师范大学计算机科学系,甘肃兰州730070)摘要:重点讨论了与程序验证相关的问题,并结合已有的求取循环不变式的方法给出了求已知循环程序的循环不变式的原则。关键词:程序;程序验证;Hoare逻辑;循环不
2、变式中图分类号:TP311.1文献标识码:A程序的正确性一直是设计者和使用者最为关心的问题,对相关问题的讨论将有助于对问[1]题的理解。Hoare公理是证明程序正确性的一种形式化方法,在证明循环程序过程中,循环不变式起着至关重要的作用。因此,它的寻找方法也是大家非常关心的问题。1程序从程序员的角度上讲,程序就是为了解决某实际问题的,用某种语言表示的一个有限指令序列;从逻辑的角度上理解,具体的一种计算机语言,就是符号逻辑中的一阶语言,计算机语言中的语法规则就是一阶语言中Lt的具体体现;语句就是一阶语言中的公式,程序
3、就是定义于此一阶语言的一个结构。2程序规范在软件生存期的整个过程,可细分为系统分析和规范定制。设计、编码、调试、运行维护五个阶段。这五个阶段每一个都是必不可少的。其中的规范定制尤其如此,在软件设计过程中起着承上启下的作用。规范是软件所需要满足的需求和目的的体现,它是一种易于理解的精确而形式的陈述。以便恰当地体现需求。规范由两部分组成。第一,性质规范是属性的形式陈述。一般属性涉及安全性、可靠性、健全性和有效性,它定义了程序对所有可能的执行必须具备的特征。第二,功能规范是功能需求的形式陈述。功能需求描述程序的需求行为
4、。当然,程序规范的两部分用相同的形式方法陈述。一般地,程序规范描述程序要达到“什么”,而不描述“如何”达到。也就是说规范以结果的形式描述行为。例:考虑把数组的所有元素置为零,程序段如下:i:=0;dowhilei<=10a[i]:=0:i:=i+1而规范描述为:(ai∈A)(ai=0)在实现中抽象掉数组的长度和元素置零的次序。通常,设收稿日期:2000-01-18基金项目:甘肃省教委科研基金资助项目(991-22)44甘肃科学学报2000年第3期计的程序是有一定的适用范围的。为了确切体现程序不仅在执行后应满足结果
5、的描述,而且程序应该满足前提条件的形式描述。为此可把{P,Q}记为程序的规范。其中,P表示前提条件又称为前断言,Q表示结果的形式描述。3程序验证程序员从早期程序设计起,就面临要证明他们的程序达到某种预定目的的任务,这就是程序验证。为此目的,人们使用了各种各样的方法,其中使用较早及较多的是测试方法。然而,测试方法有它的局限性,它只能说明程序有错而不能证明程序是正确。因此,为了保证程序的正确性,必须从理论上研究有关“程序正确性证明”的形式化的方法。这一方面的研究早在50年代就为Turing等人所注意。开展了一些早工作
6、,60年代后期Floyd,Hoars,Manna等人提出不变式和公理方法。70年代以来又发展许多验证方法,利用这些方法不仅可以证明顺序程序的正确性,而使用某些方法还可以证明非确定程序及并行程序的正确性。程序是初始状态变换到最终状态的算法描述,变换过程为程序的执行。于是程序P的执[2]行可看成函数E,其定义域是P的合法的初始状态集合,其值域是P的合法的最终状态的集合。把函数E称为执行函数,并且由h表示程序的合法初始状态集合的条件,由j表示程序的合法最终状态集合的条件,其中h和j表示程序P的状态空间D=D1×…×Dn
7、的诸子空间条件,子空间由程序P引用的数据对象Qi的值域Di定义,如果E(P,do)有定义,则在初始状态do下执行程序P产生的最终状态fd是f=E(P,do),对初始状态do,如果P对do不终止,则E(P,do)无定义,并且如果P对do终止,则E(P,do)为最终状态。程序可能因地址出错,非法指令、算术错误、无限循环等而不终止。这样E(P,do)是一个部分函数,因为对某些初始状态而言,它可能无定义。程序执行结果,即程序语义,以初始状态与最终状态之间的差异来定义。程序执行的语义性质的陈述通常描述在一大类合法初始状态的
8、集合上的执行函数E。使用记号{h}P{j}表示“如果初始状态do满足h(即如果h(do)则程序终止,并且最终状态满足j(即j(df))”。程序的正确性分为完全正确性及部分正确性。完全正确性是指:对任何一组允许的输入do,即h(do)为真,程序能终止且程序执行得到的状态满足j(j(df)),则说程序P是完全正确的。程序的部分正确性是指:对任何满足h的输入do,若程序执行能在
