基于符号计算方法的程序验证技术研究.pdf

文档介绍：华东师范大学
博士学位论文
基于符号计算方法的程序验证技术研究
姓名:武斌
申请学位级别:博士
专业:系统分析与集成
指导教师:杨路
20100301
摘要程序验证足计算机程序设计领域的前沿研究课题,,随着符号计算理论的不断完善和程序验证中使用精确无误差的数学方法的要求,:循环不变式生成、,设计了一个多项式时问复杂度的循环不变式自动生成算法,,确定循环条件在循环次数充分大时的符号,,,,设计了一个高效、,,在循环次数充分大时,判断循环条件的符号,、,对于可求出闭形式解的非线性赋值循环程序以及运算可交换的多分支循环程序,也做了研究结果表明,符号计算足验证程序氯沸缘囊恢中兄行У姆椒ǎ颐瞧诖将符号计算中的一些经典算法更深入、广泛地应用到程序验证,并集成、研发新的关键词:程序正确性,程序验证,循环不变式,终止性分析,前置条件,.
琣,甧.,.,,篻,畐.,甌.—,篐瑆..琍,琓,,
武斌博士学位论文答辩委员会成员名单姓名备注周巢尘朱惠彪教授华东师范大学职称单位研究员中张晓东上海交通大学刘静郁文生
第一章绪论程序验证茄芯砍绦蛘沸缘睦砺郏慵扑慊绦蛏杓领域的传统研究课题,但迄今为止,对常见的绝大多数程序而言,实现完全的『,随着计算机应用范围的日益扩大和计算机程序设计语言的迅速发展,如何保汪程序的正确性、提高软件的可信度一直足计算机科学界高度关注的一个重要问题,,,为了检测一个程序足否正确地实现了预定的目标,通常使用两种方法:’些初始数据,试验性地执行这个程序,,就检查和修改所编写的程序,直至对所有规定的初始数据,,程序对不同的初始数据的加工过程足不同的,,使用测试方法穷尽程序的各种可籌过程以确保程序的正确性,,“测试方法只能发现程序的错误,而不能确保程序无误绦蜓橹ぷ阊究程序正确性的理论,是研究如何使用数学方法严格证明程序所有可能的初始数据都足符合其预定目标的,,ê,,通常程序验证的工作量更大,但足验证技术也具有更多的优·应用程序验证技术,我们可以在更深地层次洞察程序,并且能够帮助我们真正理解程序的思想以及它的局限性浚·程序验证技术可以更好的支持面向目标的程序开发浚由此可见,程序验证足保证程序正确性的一个基本而重要的手段,:
程序正确性研究方法概述明和验证的方法之一——公理化方法..,,由于程序验证中数学证明的复杂性,研究热度有所下降,甚至许多悲观的研究者认为程序验证的理论