Larch/C++ is a notation for formally specifying the behavior and interfaces of C++ classes and functions. C++ is the programming language defined in Stroustrup’s book [Stroustrup91](1) and more fully in Ellis and Stroustrup’s book [Ellis-Stroustrup90] and the draft C++ standard [ANSI95]. These contain the reference manual for C++. The goal of this reference manual is to precisely record the design of Larch/C++.
Book Description
We try to give examples and explanations, and we hope that these will be helpful to readers trying to learn about formal specification using Larch/C++. However, this manual is not designed to give all the background needed to write Larch/C++ specifications, nor to give the prospective user an overview of a useful subset of the language.
Table of Contents
- Introduction
- Fundamental Concepts
- Syntax Notation
- Lexical Conventions
- Declarations
- Function Specifications
- Class Specifications
- Template Specifications
- Specification Modules
- Refinement
- Built-in Types