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

项目名称： 面向对象程序的分离逻辑理论基础

项目编号： No.61272160

项目类型： 面上项目

立项/批准年度： 2013

项目学科： 自动化技术、计算机技术

项目作者： 裘宗燕

作者单位： 北京大学

项目金额： 80万元

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

中文关键词： 形式化建模与验证；面向对象程序；分离逻辑；验证工具；程序验证和测试

英文摘要： 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, dat

英文关键词： Formal Modeling and Verification；Object-Oriented programs；Separation Logic；Verification Tool；Program Verification and Testing