Formal Specification for C++ Programs

这个项目的目标是：帮助程序员用面向对象的编程语言C++形式化地指定模块的接口，并帮助程序员对使用消息传递和继承的程序的正确性进行推理。规范方面的工作将涉及为C++设计和正式定义接口规范语言，并在几个示例中测试规范语言的实用性。规范语言LARCH/C++将使用子类型关系和断言中的重载来指定多态模块。验证工作将涉及基础研究，以理解规范语言应该能够表达的属性。这些属性包括规范之间的关系，如细化和子类型、如何在规范中使用继承以及推断突变和别名的方法。虽然这样的研究最终可能导致C++程序验证的正式方法，但重点将是学习如何指定需要证明的属性。该项目将促进设计和程序模块的重用，并将有助于指导对C++程序的推理。开发的技术也将适用于其他面向对象的语言。

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.