In a init-declarator-list, one can specify an initial value for a variable just as in C++. The syntax for an expression, constant-expression, and assignment-expression is exactly as in C++ (see Sections 17.2 of [Ellis-Stroustrup90] and [ANSI95]), and so is not given here.
initializer ::==constant-expression |={initializer-list}|(expression-list)constant-expression ::= exactly as in C++ initializer-list ::= initializer-clause [,initializer-clause ] ... [,] initializer-clause ::= assignment-expression |{[ initializer-list ] } assignment-expression ::= exactly as in C++ expression-list ::= expression [,expression ] ... expression ::= exactly as in C++
For example, one can use each of the following lines as an initializer.
= 7 = 6.5e-7 = 'c' = "a string"
If one wishes to abstractly specify the initial value,
instead of giving C++ code,
then one can write a fun-spec-body
to specify the value.
For example, if the class IntHeap has been specified
with abstract values from trait IntHeapTrait
(see section 1.1 Larch-style Specifications),
then one can write a declaration such as the following
to specify the initialization of the variable myHeap
to the abstract value add(3, (add 4, empty)).
// @(#)$Id: abstract-init.lh,v 1.1 1997/01/10 23:29:38 leavens Exp $
#include "IntHeap.lh"
IntHeap myHeap;
//@ behavior { ensures myHeap' = add(3, add(4, empty)); }
Go to the first, previous, next, last section, table of contents.