面向对象程序的分离逻辑理论基础

Object-Oriantation (OO) is one of the main stream techniques in software development. However, its theoretical foundation is relatively weak, and there is no widely respected and effective formal verification technique for it. This is one reason why the OO techniques are completely rejected by the safety-critical software development fields. Now a day, the requirements for the correctness and reliability of computer systems from the society is even higher. To satisfying this requirements, and giving free rein to the great potentials of the OO techniques, the fundamental theories and formal verification techniques for supporting OO software development need to be invectigated. This proposal makes its focuses on the application of the ideas and techniques of Separation Logic to the formal theory of OO programs and their verification. It pursues to the building of suitable logical assertion language for OO programs and powerful verification framework based on the logic language, as well as the development of tools for supporting the vefication. The proposed research will base its work on the logical theories of the procedural programs and the new development of Separation Logic. In the work, all the most important features of OO porgrams, e.g., subclasses and subtypes, inheritance, overridding, dynamic binding, data abstraction, etc., their theoretical and verification problems will be the central consideration. In addition, the logical theory will be developed formally based on some proof assistant system. The final potantial and application of the work is the power and widely usable logic framework for the modular verification of OO programs, to satisfy the requirements of the correctness verification of systems which are developed using OO techniques.

面向对象（OO）是软件开发的主流技术，但其理论基础薄弱，尚无被广泛认可的有效形式化验证技术，这是OO技术被安全苛求软件开发领域完全排斥的一个重要原因。为更好满足社会对软件系统正确性和可靠性越来越强烈的需求，进一步发挥OO技术的巨大潜力，需要研究能很好支持OO软件开发的基础理论和形式化验证技术。本项目研究分离逻辑的思想和技术在OO程序的形式化理论和程序验证领域的应用，为OO程序建立合适的逻辑断言语言和基于该逻辑语言的较完整的OO程序验证理论，并将进一步开发支持OO程序验证的工具。本项目工作将参考过程式程序的逻辑理论和分离逻辑的最新成果，特别关注OO程序的各种重要特征，包括子类和子类型、继承、覆盖、动态绑定、数据抽象等的理论问题和验证技术，并基于定理证明器开发严格形式化的逻辑理论。其应用目标是开发适用面广的OO程序模块化逻辑验证框架，以满足基于OO技术的系统的正确性验证的需要。

本项目基于我们以前在自然科学基金支持下开展的与面向对象程序的分析与验证有关的研究工作。本项目围绕面向对象程序的验证、分离逻辑在面向对象程序建模和验证方面的应用、面向对象程序的分离逻辑验证系统和工具实现，以及一些与此有关的形式化理论和模型方面的问题开展了研究工作，取得了一批成果。主要成果包括：针对面向对象程序中抽象机制的建模和验证问题开发了基于分离逻辑的验证框架和验证方法；提出了类中方法中间相互关系的验证模型；开发了分布式程序的分离逻辑模型和验证方法；提出了面向对象程序中拥有权关系的自动分析、标注和验证方法。特别是基于辅助证明器Coq开发了一个面向对象程序的验证系统，集成实现了我们在以前基金项目和本项目研究工作中的成果，并用这个系统验证了一些程序实例。除了上述工作，我们还研究了面向对象程序测试实例的形式化生成、连接件的建模和验证问题等。至今在国际会议和杂志发表标注论文18篇。有关方面的工作为面向对象程序的验证和计算机程序与系统的形式化建模和验证提供了一些新的认识和基础性理论，为验证工具的开发提供了想法和经验。