A Theoretical and Practical Basis for Applying Formal Methods to Object-Oriented Programming and C++

本研究旨在为指定和验证面向对象程序提供理论基础，并为在编程语言c++中使用形式方法提供实践基础。该项目扩展了抽象数据类型的模型理论和证明理论，以帮助描述一个抽象数据类型何时是另一个抽象数据类型的行为子类型。以前的工作已经为具有不可变对象的抽象数据类型之间的行为子类型提供了充分的条件。这些条件基于类型规范，反映在这些规范的代数模型中。行为子类型允许对程序进行模块化规范和验证，使用静态类型信息而不需要对每个子类型进行用例分析。另外，证明了子类型关系满足行为子类型的语义条件。一个重要的问题是为对象具有时变状态（即可变）的抽象类型的行为子类型找到必要和充分条件，因为这些类型在实践中经常出现。需要证明来自类型规范的行为子类型关系的方法。本研究将模块化规范和验证工作扩展到具有突变和非确定性的语言。实际工作的目的是为快速增长的c++程序员社区提供使用这种语言的形式化方法的基础。对于代码的系统开发、程序验证、代码重用和其他正式的开发活动来说，必不可少的是一种正式的规范语言。本项目推进Larch/ c++，并为c++模块量身定制接口规范语言。包括针对Larch/ c++的类型检查器在内的工具，以及一套教材、教程和更大的工作示例正在开发中。

This research seeks a theoretical foundation for specifying and verifying object-oriented programs, and a practical foundation for the use of formal methods with the programming language, C++. The project is extending the model theory and proof theory of abstract data types to help characterize when one abstract data type is a behavioral subtype of another. Previous work has given sufficient conditions for behavioral subtyping among abstract data types with immutable objects. These conditions are based on type specifications, as reflected in algebraic models of these specifications. Behavioral subtyping allows modular specification and verification of programs, using static type information without using case analysis for each subtype. Separately, one proves that the subtype relationships satisfy the semantic conditions of behavioral subtyping. An important problem is to find necessary and sufficient conditions for behavioral subtyping for abstract types whose objects have time-varying state (i.e., that are mutable), since these types occur frequently in practice. Needed are ways to prove behavioral subtype relationships from type specifications. This research would extend the work on modular specification and verification to languages with mutation and non-determinism. The practical work is aimed at providing the fast-growing community of C++ programmers with a foundation for the use of formal methods with this language. Essential to systematic development of code, program verification, code reuse, and other formal development activities, is a formal specification language. This project advances Larch/C++, and interface specification language tailored to specify C++ modules. Tools, including a type-checker for Larch/C++, are being developed, as are a suite of teaching materials, and tutorial and larger worked examples.