论文摘要
面向对象(OO)程序语言和开发方法的发展较好满足了软件规模快速发展的需要,带来了计算机软件领域的重大变革。近年来,随着社会对软件系统可靠性和正确性要求的不断增强,开发出行之有效的支持OO程序的开发和验证的技术变得越来越重要和紧迫。为开发强大而实用的OO程序验证系统,必须考虑两个互相依赖的问题:第一,为OO语言定义一个形式化语义。该语义应能处理各种重要的OO特性,如继承,动态方法绑定等;它应足够高级以支持深入的理论研究,又能指导实际验证系统的开发和实用化。第二,开发有效的描述和验证OO程序的技术,既能有效支持程序的验证过程,又使程序的描述和验证可以以模块化的方式进行,从而提高可能验证的程序的规模。本文以开发实用的OO程序验证系统为研究目标,以模型语言μJava为参考研究对象,考查了上述两个问题。μJava是Java的一个串行子类,它包含了许多关键的OO特性,例如引用语义,对象共享,继承和动态方法绑定等,因此是具有典型性和代表性的研究对象。本文首先提出了一个通用的面向对象存储模型,并在此基础上定义了一个面向对象的Separation Logic(OOSL),用以描述OO程序的执行状态。进而以该逻辑作为描述程序状态的断言语言,为μJava定义了一个最弱前条件语义,证明了该语义的许多良好性质,包括其可靠性和完全性。以这一语义为基础,本文研究了OO程序验证中的许多基本问题,如方法规范,对象不变式,行为子类型等。本文还着眼于实际可用的验证系统,为此在前面工作的基础上逐步扩展μJava,为其加入了丰富的规范描述结构用以描述程序的行为,开发了一个验证框架来检验OO程序是否满足用户提供的规范。所开发的验证框架能支持OO程序的模块化规范描述和验证,避免重复验证代码。文中通过一些典型OO程序实例,说明了OO程序的规范描述和验证工作可能如何在此验证框架下很好进行。文中也将提出的技术与国内外相关工作做了深入细致的对比。本文涉及到了当前的许多研究热点,包括Separation Logic,抽象规范,模块化验证等,在这些方面本文紧跟着理论前沿提出自己的见解;而在一些人们长期关注的理论问题上,例如OO程序的存储模型,对象不变式等问题上,也有些新的认识和观点。综上所述,本文中给出的OO程序验证技术更易于理解,也更贴近工程实践,对开发实用的OO程序验证工具有很好的指导意义。