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.