In a Larch/C++ specification, a declaration plays two roles. As usual, it introduces one or more names into a specification and gives information about the name's type and other attributes, which are used in giving meaning to occurrences of the name. But in addition a declaration specifies that the C++ module that implements the specification must have the same declaration. (The only exceptions are ghost variable declarations, see section 9.1 Ghost Variables, and the declarations in the declaration-seq of a Larch/C++ function specification, see section 6.7 Global Variables.) This is in accord with the principle of behavioral interface specification (see section 2.2 Interfaces). Therefore, by giving a declaration in Larch/C++, one can specify the storage class, type, and linkage for an object, and the type and linkage for functions. One can think of the declaration as going directly into the C++ code. (This is easily accomplished if the specification is given as annotations in a C++ header file.) Because of this, the declaration must satisfy the restrictions on C++ code in Section r.7 of [Stroustrup91].
The syntax of a declaration in Larch/C++ is nearly identical to the syntax of a declaration in C++. The only difference is that additional forms that are useful in specifications are permitted, and specification information can be attached to various productions. In particular, Larch/C++ adds the ability to declare the behavior of functions (see section 6 Function Specifications) and classes (see section 7 Class Specifications). Larch/C++ also adds the ability to pass traits to templates (see section 8 Template Specifications) and higher-order functions (see section 6.13 Specifying Higher-Order Functions).
Thus the Larch/C++ syntax is a superset of the C++ syntax for declarations. The Larch/C++ syntax is given below.
declaration ::= [ decl-specifier-seq ] [ init-declarator-list ];[ fun-spec-body ] | [ decl-specifier-seq ] ctor-declarator [ fun-spec-body ] | block-declaration | function-definition | template-declaration | explicit-instantiation | explicit-specialization | linkage-declaration | namespace-definition | refinement-declaration |externeverything;block-declaration ::= asm-definition | namespace-alias-definition | using-declaration | using-directive init-declarator-list ::= init-declarator [,init-declarator ] ... init-declarator ::= declarator [ initializer ]
Other sections of this chapter give more information on the parts of a standard C++ declaration: decl-specifier-seq, declarator, and initializer. The decl-specifier-seq give the type and other information about the thing being declared. The declarator gives the name of the thing being declared, and may also give information about whether the thing being declared is a pointer, array, or function. An initializer allows one to declare an initial value.
Other parts of the C++ declaration syntax that recursively
use declarations are
treated in subsections of this chapter:
linkage-declaration,
namespace-definition, and namespace-alias-definition.
See section 5.4.6 Function Declarations for the syntax and semantics of
function-definition and ctor-declarator.
See section 6 Function Specifications for the syntax and semantics
of fun-spec-body.
See section 6.7 Global Variables for the meaning of
a declaration of the form extern everything;,
which is used in function specifications.
See section 8 Template Specifications for the syntax and semantics of
template-declaration.
See section 10 Refinement for the syntax and semantics of
refinement-declaration.
For example, after the initial comment, each (nonblank) line and group of lines of the following is an example of a declaration.
// @(#)$Id: declaration.lh,v 1.8 1997/06/03 20:30:01 leavens Exp $
int i;
int j = 3, k = 4; // declaration with initializers
int *ip = &i;
extern double Sqrt(double x);
static int zero = 0;
typedef int *IntPtr;
class MyClass { MyClass(); }; // class with ctor-declarator
int zero() throw() { return 0; } // function-definition
int one() throw() // function-definition
//@ behavior { ensures result = 1; } // with fun-spec-body
{ return 1; } // and fun-body
template <class T> // template-declaration
extern T Id(T x) throw();
//@ behavior { ensures result = x; } // with fun-spec-body
//@ refine zero by // refinement-declaration
int zero() throw();
//@ behavior { ensures result = 0; }
extern "C" double ceil(double x); // linkage-declaration
namespace long_name { int x; } // namespace-definition
namespace n = long_name; // namespace-alias-definition
asm ("add r1,r2"); // asm-definition
Go to the first, previous, next, last section, table of contents.