The unit of specification in Larch/C++ is the interface. Note the difference between the uses-clause, which specifies an abstract model through some traits, and the using-declaration and the using-directive, which have to do with C++ "namespaces" [Stroustrup95]. (See section 5.5 C++ Namespace and Using Declarations for the syntax of the latter.)
An interface consists of a possibly-empty sequence of top-level declaration forms.
interface ::= top-level [ top-level ] ...
top-level ::= uses-clause | spec-decl | depends-clause
| represents-clause | invariant-clause | constraint-clause
| declaration | using-declaration | using-directive
A C++ program file implements an interface if it has the same interface (see section 2.2 Interfaces) and if for each specified declaration there is a definition that satisfies it. The spec-decls do not have to be implemented. See section 9.1 Ghost Variables for a description of their uses.
See section 7 Class Specifications for the syntax and semantics of invariant-clause an and a constraint-clause. (Used at the top level, such clauses allow one to state invariant and history properties of global variables.) See section 5.5 C++ Namespace and Using Declarations for the syntax and semantics of using-declaration and using-directive.
The other top-level declaration forms are explained below.
Go to the first, previous, next, last section, table of contents.