Promela |
Declarator |
arrays(2) |
NAME
arrays
-
syntax for the declaration and initialization of one-dimensional
arrays of variables.
SYNTAX
typename name '['
const ']'
[ =
any_expr ]
DESCRIPTION
An object of any datatype, predefined (see
datatypes(2), chan(2)) or user-defined (see
typedef(2), mtype(2)), can be declared either as a scalar, or
as an array of similar elements.
The array elements are distinguished from one another
by their array index. As in the language
C, the first object in the array always has index zero.
The number of objects in the array must be specified in the
declaration with a numeric constant
(i.e., it cannot be specified with an expression).
If an initializer is present, the initializing expression
is evaluated once and all array elements are initialized
to the same resulting value.
In the absence of an explicit initializer, all array elements are initialized to zero.
Data initialization happens in the initial system state, for globally declared variables, and in the initial process state, for process local variables. The latter is independent of where in a proctype body the variable declaration is placed.
EXAMPLES
byte state[N]with N a constant, declares an array of N bytes, all initialized to zero, that can be assigned and referred to in statements such as
state[0] = state[3] + 5 * state[3*2/n]where n is a constant or a variable declared elsewhere. An array index can be an arbitrary, side effect free, Promela expressions. The valid range of indices for array state , declared above, is 0 .. N-1 .
NOTES
Scalar objects are treated as shorthands for
array objects with a single element, meaning
that also references to scalar objects may be suffixed with
[0] ,
without triggering a complaint from the parser.
An array of bit or bool variables is stored by the verifier as an array of unsigned char , and therefore saves no memory over byte arrays.
Multi-dimensional arrays can be constructed indirectly with the use of typedef definitions. See typedef(2).
The use of an index value outside the declared range triggers a runtime error in Spin. This default array-index bound checking can be turned off during verifications (if desired for efficiency reasons) if the pan.c source is compiled with the additional directive -DNOBOUNDCHECK .
SEE ALSO
chan(2), mtype(2), datatypes(2), typedef(2).
|
Spin Online References Promela Manual Index Promela Grammar Spin HomePage |
(Page Updated: 16 December 1997) |