Promela Reference -- assignment(4)

Promela

Basic Statement

assignment


NAME
assignment - for assigning a new value to a variable.

SYNTAX
varref = any_expr
varref ++ as shorthand for varref = varref +1
varref -- as shorthand for varref = varref -1

EXECUTABILITY
true

EFFECT
Replaces the value of varref with the value of any_expr , where necessary truncating the latter value to the range of the datatype of varref .

DESCRIPTION
The assignment statement has the standard semantics from most programming languages: replacing the value stored in a data object with the value returned by the evaluation of an expression. Other than in the C language, the assignment as a whole returns no value and can therefore itself not be part of an expression.

The variable reference that appears on the left-hand side of the assignment operator can be a scalar variable, an array element, or a structure element.

EXAMPLES

Note that it is not valid to write: because the right-hand side of this assignment is not a side effect free expression in Promela, but it is shorthand for another assignment statement. The effect of this statement can be obtained, though, by writing: or even more efficiently: Similarly, there are no shorthands for other C shorthands, such as ++b , --b , b *= 2 , b += a , etc. Where needed, their effect can be reproduced by using the non-shortened equivalents, or in some cases with atomic or d_step sequences.

NOTES
There are no compound assignments in Promela, e.g., assignments of structures to structures or arrays to arrays in a single operation. If x and y are structures, though, the effect of a compound assignment could be approximated by passing the structure through a message channel, for instance as in:

All variables must be declared before they can be referenced or assigned to. The default initial value of all variables is zero.

SEE ALSO
arrays
condition
datatypes
typedef


Spin Online References
Promela Manual Index
Promela Grammar
Spin HomePage
(Page updated: 28 November 2004)