论文部分内容阅读
面向对象程序有着远比过程性程序丰富的结构和特征，因此给程序的验证带来了许多新的挑战和问题。本文研究面向对象程序验证相关的一些的理论和技术。 面向对象程序的一个基础是语言的引用语义。引用带来的对象共享提高了语言的表达能力，对于实际面向对象程序是必不可少的。对象共享带来的问题是运行中广泛存在的别名问题，然而未有任何限制和管理的别名不仅会使程序难以理解，还可能带来不易发现的程序错误，威胁软件系统的可靠性和安全性，也给面向对象程序的严格检查和验证带来很大困难。为处理复杂的面向对象结构，以及复杂的面向对象程序的验证，人们进行了许多研究，一方面设法实现对程序中潜在别名的静态封装管理，同时探讨相应的程序理论和程序验证基础。 面向对象程序中的别名控制问题的研究已有二十多年历史，人们提出了一些处理和解决该问题的想法和技术，主要方法是希望通过对程序语言或者程序逻辑进行设计或扩展，以支持对可能存在别名的程序的分析、推理和验证。在设计原则上，既要考虑相关检查技术的能力和代价，也要结合开发实践的需求，努力提供便于实际开发者理解和实现的模型。目前已有的别名控制技术大多都能保证对程序良好封装性质的静态检查，基本方法是在语言中加入标注关键字，建立一套增强的规则或类型系统。在设计有关技术时，因为既要考虑对别名问题的解决，又要考虑面向对象语言的特性，所以得到的框架都比较复杂，至今尚未有一种技术被广泛认可并增加到实际的程序语言中。融合静态类型系统、程序验证技术和动态断言检查等技术来进行程序验证的方法也在讨论研究中。 本文一方面的工作讨论并建立了面向对象程序的对象封装框架的一种技术，它能支持静态实现的别名管理。本工作基于一个具有面向对象语言主要特征的模型语言，提出了一套封装需求描述的标记方法。这一方法的主要特点是从对象使用者类的角度出发描述别名控制，提供一种路径表达式来描述封装关系，其技术路线有别于已有的对象封装和别名控制技术，具有新颖性。文中对于封装描述提出的性质要求既是封装良好的保证，又可作为程序员书写封装描述的指导。 论文中进一步开发了一套类型规则，建立了用于静态检查的类型系统，说明这种封装框架下的程序良好封装性质同样可以静态检查。文中还证明了这一类型系统的可靠性。可靠性证明是基于一个关于封装的语义模型。证明方法及过程简单、清晰。文中工作是面向对象语言的类型及类型系统理论研究方面的一种新思路。 本文工作是对已有静态别名分析理论和技术的一个应用。部分方法内的别名分析结果处理后的别名关系集辅助于封装描述良形式和方法调用规则定义，在一定程度上简化了程序中的封装描述，因而只需描述需要封装的内容，同时也保证了检查的模块性。文中还将提出的方法与本领域最重要的拥有者类方法进行了深入细致的比较和讨论。 本文还提出了一种程序验证抽象规范描述的正确性的检查方法，提出通过验证程序的抽象规范与代数规范的一致性来说明程序中抽象规范的正确性。 论文最后总结并探讨了进一步的研究工作。