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.