Larch/C++ Reference Manual
DRAFT, $Revision: 5.41 $
12 April 1999
by Gary T. Leavens
1 Introduction
1.1 Larch-style Specifications
1.2 What is Larch/C++ Good For?
1.3 Status and Plans for Larch/C++
1.4 Larch/C++ Tools
1.4.1 Obtaining and Installing the Larch/C++ Release
1.4.2 Obtaining LSL and LP
1.4.3 Typical Use of the Tools
1.5 Acknowledgements
2 Fundamental Concepts
2.1 Viewpoint
2.2 Interfaces
2.3 Accessibility of Class Members in Specifications
2.4 Modules and Files
2.5 Declarations and Definitions
2.6 Scope Rules
2.7 Types and Sorts
2.8 Objects and Values
2.8.1 Formal Model of Objects
2.8.1.1 Formal Model of Mutable Objects
2.8.1.2 Formal Model of Constant Objects
2.8.2 Formal Model of States
2.9 Satisfaction
3 Syntax Notation
4 Lexical Conventions
4.1 White Space
4.2 Comments
4.3 Annotations
4.4 Pragmas
4.5 Tokens
4.6 Identifiers
4.7 Simple-Ids
4.8 Keywords
4.9 Context-Dependent Keywords
4.10 Special Symbols
4.10.1 Always Special Symbols
4.10.2 C++ Declaration Symbols
4.10.3 C++ Operator Symbols
4.10.4 Predicate Special Symbols
4.10.5 LSL Operators
4.11 Keywords in Predicates
4.12 Informal Comments
4.13 Literals
4.13.1 Integer Constants
4.13.2 Floating Constants
4.13.3 Character Constants
4.13.4 String Constants
4.13.5 Abstract String Constants
4.14 LSL Constants
4.15 Alternative Tokens
5 Declarations
5.1 Initializers
5.2 Declaration Specifiers
5.2.1 Storage Class Specifiers
5.2.2 Function Specifiers
5.2.3 Type Specifiers
5.2.3.1 Simple Type Names
5.2.3.2 Class and Namespace Names
5.2.3.3 Elaborated Type Specifiers
5.2.4 Friend
5.2.5 Typedef Specifiers
5.3 Enumeration Declarations
5.4 Declarators
5.4.1 Reference Declarations
5.4.2 Pointer Declarations
5.4.3 Array Declarations
5.4.4 Structure and Class Declarations
5.4.5 Union Declarations
5.4.6 Function Declarations
5.4.7 Constant Declarations
5.4.8 Summary of Declarations
5.5 C++ Namespace and Using Declarations
5.6 Linkage Declarations
5.7 Asm Definitions
6 Function Specifications
6.1 Predicates
6.1.1 If then else
6.1.2 Logical Connectives
6.1.3 Equality Terms and Quantifiers
6.1.3.1 Equality Terms
6.1.3.2 Quantifiers
6.1.4 Informal Descriptions
6.1.5 LSL Operator Terms
6.1.6 Brackets and Braces
6.1.7 Primaries
6.1.8 Primitives
6.1.8.1 Sorts for Formal Parameters
6.1.9 Primary Suffixes
6.1.10 Larch/C++ Special Primaries
6.1.10.1 This and Self
6.1.10.2 Result
6.1.10.3 Names of States (pre, post, and any)
6.2 Mutation
6.2.1 State Functions
6.2.2 Allocated and Assigned
6.2.3 The Modifies Clause
6.2.3.1 Constructs
6.2.3.2 Syntactic Sugars in the Modifies Clause
6.2.3.3 Modifies and Const
6.2.3.4 Formal Details of the Modifies Clause
6.2.3.5 Reach
6.2.3.6 Unchanged
6.3 Allocation and Deallocation
6.3.1 Fresh
6.3.2 The Trashes Clause
6.3.2.1 Trashed
6.3.2.2 Formal Details of the Trashes Clause
6.4 The Calls Clause
6.5 The Accesses Clause
6.6 Default Arguments
6.7 Global Variables
6.8 Let Clauses
6.9 Redundancy in Function Specifications
6.9.1 Examples in Function Specifications
6.9.2 Redundant Requires Clauses
6.9.3 Redundant Ensures Clauses or Claims
6.9.4 Redundancy in Frames
6.10 Case Analysis
6.11 Exceptions
6.12 Liberal Specifications
6.12.1 Terminates
6.12.2 Liberal Specification and Case Analysis
6.12.3 Examples of Liberal Specification
6.12.4 Meaning of Function Specifications
6.13 Specifying Higher-Order Functions
6.14 Behavior Programs
6.15 Annotated Iteration Statements
7 Class Specifications
7.1 Examples of Class Specifications
7.1.1 A First Class Design (Person)
7.1.2 A Design with a Nontrivial Trait (Money)
7.1.3 A Class with Exceptions (Stack)
7.2 Class Member Specifications
7.2.1 Constructors
7.2.2 Destructors
7.2.3 Implicitly Generated Member Specifications
7.3 Class Invariants
7.4 History Constraints
7.5 Contained Objects
7.6 The Depends Clause
7.7 The Represents Clause
7.8 Specifying Derived Classes
7.9 Inheritance of Specifications and Subtyping
7.9.1 Inheritance of Specifications with Specification Variables
7.9.2 Inheritance with Explicitly-Given Traits and Weak Subtyping
7.9.3 More Details of Specification Inheritance
7.9.3.1 Strong vs. Weak Behavioral Subtyping
7.9.3.2 Simulation Functions that Need a State
7.9.4 Related Work on Inheritance of Specifications
7.10 Abstract Classes
7.11 Specifying Exposed Data Members
7.12 Specifying Friends
8 Template Specifications
8.1 Example Template without Requirements
8.2 Requirements on Template Parameters
8.3 Instantiation of Templates
9 Specification Modules
9.1 Ghost Variables
9.2 The Uses Clause
10 Refinement
10.1 Function Refinement
10.2 Class Refinement
10.3 Specifying Protected and Private Interfaces
10.4 Template Refinement
10.5 Namespace Refinement
10.6 Nested Refinement
11 Built-in Types
11.1 Integer Types
11.1.1 Signed Trait
11.1.2 Short Integer Trait
11.1.3 Long Integer Trait
11.1.4 Char Trait
11.1.5 int Trait
11.1.6 Unsigned Integer Trait
11.1.7 Summary of Trait Functions for Integer Traits
11.2 Wide Characters
11.3 Floating Point Types
11.4 bool
11.5 void
11.6 Enumeration Types
11.7 Array Types
11.8 Pointer Types
11.9 Character Strings
11.10 Structure and Class Types
11.11 Union Types
11.12 Function Types
A Grammar Summary
11.13 Lexical Conventions
11.14 Declarations
11.15 Function Specifications
11.16 Class Specifications
11.17 Template Specifications
11.18 Specification Modules
11.19 Refinement
B Bibliography
C Differences
C.1 Differences Between Larch/C++ and Larch/C
C.2 Differences Between Larch/C++ and C++
D Deprecated
D.1 Deprecated Syntax
Example Index
Concept Index
This document was generated on 12 April 1999 using the
texi2html
translator version 1.50.