摘 要: 介绍了Dijkstra的形式化推导方法的主要思想、步骤及要点。该方法主张程序开发和程序证明同时进行,先确定好描述程序功能的断言,再通过形式化方法推导出正确的程序。选择具有代表性的循环结构的实例进行推导证明,并对循环结构的形式化推导进行阐述说明。
关键词: 形式化方法;程序正确性;循环不变式;界函数
算法是计算机科学的核心,而算法的正确性是近几年讨论的热点问题,但是效果并不明显。一般情况下,程序的正确性都是针对已经编好的程序,通过测试用例,尽可能地找出程序的漏洞,但这种方法并不能从根本上保证程序的正确性。采用形式化的方法[1]来进行设计程序,是先将需要解决的问题精确描述出来,再根据某种形式化规则进行推理,最终得到正确且结构化的程序。目前存在很多种形式化方法,Dijkstra的最弱前置条件程序推导;英国爱丁堡大学的Burstall和Darlington所研制的ZAP系统;基于公理语义的Z;基于指称语义的VDM;基于抽象机的B方法;江西师范大学提出的PAR(Partition And Recur)方法[2-5]等。
如果能找出一套形式化方法,实现程序的自动化开发和证明,将使得开发周期大大缩短,降低程序开发的成本,也将不再有后期维护的后顾之忧。Dijkstra主张程序开发和程序证明同时进行,属于半自动化的形式化方法[6]。需要人为地找出确定描述程序功能的断言、循环不变式以及t函数。若能提出某种方法实现此过程的自动化,将有望找出自动化的形式化推导。
1 形式化推导的基本思想
1.1 {Q}S{R}系统
设S是一个程序语句,S的前断言为Q,后断言为R,记法{Q}S{R}表示如果在S执行之前谓词Q为真,那么在S执行之后谓词R也真[7]。
1.2 最弱前置条件wp(S,R)
对于给定的程序S,wp(S,R)是一个状态集合,以该集合中任一状态作为初始状态执行程序S都能保证程序终止且满足后置条件R;反之,能使程序终止,且终止状态满足后置条件R的初始状态必属于wp(S,R)所定义的状态集合。即对程序S来说,wp(S,R)是属于后置条件R的最弱前置条件。
1.3 空语句
“skip”表示空语句,即什么都不执行。
严格按照形式化推导的方式开发得出循环结构,保证了此程序的完全正确性。
本文简要介绍了Dijkstra的最弱前置条件程序推导方法,并通过开发并证明任意正整数的阶乘来说明此方法的步骤及其要点。此例子中,需要人为地寻找出后置条件R、循环不变式P、以及t函数。自动化的方式推导出R,P或t函数可以作为下一步的研究课题。而自动化生成正确的程序是一个长期性的国际难题,是一项富有创造性和挑战性的活动,值得进一步研究更多的算法,寻找形式化推导的一般规律,尽可能将创造性劳动变为非创造性劳动,使形式化方法走出实验室,给工程程序的开发带来帮助。
参考文献
[1] 唐稚松,林惠民.功能描述导引的程序综合[M].北京:中国学术期刊电子出版社,1983.
[2] 石海鹤,薛锦云.基于PAR的算法形式化开发[J].计算机学报,2009,32(5):982-991.
[3] 王昕,袁超伟.一种安全协议的形式化分析方法[J].计算机工程,2010,36(7):82-84.
[4] 杨晨,薛锦云,苏昭.三个经典数学问题的形式化开发[J].计算机与现代化,2010,180(8):1-4.
[5] 王昌晶,薛锦云.算法及其时间复杂度可同步形式化推导的方法[J].计算机应用研究,2008,25(3):681-683.
[6] WYBE D E. A Discipline of programming[M]. America,1976.
[7] 杨帆,翟岩慧,曲开社,等.基于形式概念分析的词义解释研究[J].计算机科学,2011,38(10):189-191.
[8] 雷富兴,张来顺,石荣刚,等.循环条件的形式化推导在程序验证中的应用[J].计算机工程与设计,2010,31(14):3193-1397.