面向对象程序的形式化规范与验证

面向对象（OO）技术是现代软件开发的主流技术，但OO程序的理论基础还远未成熟，影响了人们对OO程序的信任，也限制了将OO技术用于关键性软件开发的可能性。为解决这些问题，需要开发能很好支持OO程序和软件开发的形式化规范与验证技术。本项目将研究OO程序的形式化规范与验证的理论和技术，在此基础上开发程序的验证工具。为描述OO程序的规范，我们将开发支持描述OO程序的复杂数据结构和性质的逻辑语言，其中将很好处理子类型、继承、动态绑定、功能和数据抽象等OO程序的主要特征。为控制对象之间的共享和别名，我们还将建立静态封装模型，以支持建立和验证OO程序的对象不变式规范。在这些工作的基础上，本项目的最终目标是建立OO程序的模块化规范与验证框架，以适应实际大型软件系统正确性验证的需要。我们还将使用定理证明器来实现OO程序的形式化规范与验证，进行程序验证工具的开发。

本项目主要研究面向对象程序的形式化规范与验证理论和技术，并在此基础上实现程序验证工具。本项目基本完成申请书中所列的研究内容，取得的成果如下：（1）以分离逻辑为基础，定义了专门用于对类Java顺序程序进行推理验证的OO分离逻辑。另一方面，定义了类图和对象图，并在此基础上定义了以图为基础的语义和逻辑系统；（2）从用户需求出发，建立了对象的静态封装框架，从而可以根据用户意愿来控制对象共享和别名；（3）以OO分离逻辑为基础，建立了面向对象程序的模块化规范和验证理论框架，在此基础上提出了包含用户层、界面层和实现层的三层规范和验证框架；（4）以所建立的形式化规范与验证框架为基础，结合使用证明辅助器，分别实现了以OO分离逻辑和以图为基础的面向对象程序验证工具原型；（5）最后，我们将在该项目面向对象程序的规范与验证研究中所积累的理论和方法，应用到混成系统领域， 并取得了很好的成果。