Larch/C++ Reference Manual

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++.


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

Book Details

Author(s): Gary T. Leavens
Format(s): HTML
Link: Read online.

Leave a Reply