Formal Specification for C++ Programs

点击翻译按钮获取中文摘要

The objectives of this project are: to help programmers formally specify the interfaces of modules in the object-oriented programming language C++, and to help programmers reason about the correctness of programs that use message passing and inheritance. Work on specification will involve designing and formally defining an interface specification language for C++, and testing the utility of the specification language on several examples. The specification language, Larch/C++, will use subtype relationships and overloading within assertions to specify polymorphic modules. Work on verification will involve fundamental studies to understand properties that specification language should be able to express. These properties include relationships between specifications such as refinement and subtyping, how to use inheritance in specifications, and ways to reason about mutation and aliasing. While such studies may eventually lead to formal methods for the verification of C++ programs, the emphasis will be on learning how to specify the properties that need to be proved. The project would promote the reuse of designs and program modules, and would help guide reasoning about C++ programs. The techniques developed would also be applicable to other object-oriented languages.