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.
