Promela Reference -- arrays(2)





arrays - syntax for the declaration and initialization of one-dimensional arrays of variables.

typename name '[' const ']' [ = any_expr ]

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.


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 .

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 .

chan(2), mtype(2), datatypes(2), typedef(2).

Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page Updated: 16 December 1997)