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
a = 12 /* scalar */ r.b[a] = a * 4 + 7 /* array element in structure */Note that it is not valid to write:
a = b++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:
atomic { a = b; b++ }or even more efficiently:
d_step { a = b; b++ }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:
typedef D { short f; byte g }; chan m = [1] of { D }; init { D x, y; m!x; /* send structure x to channel m */ m?y /* receive and assign to structure y */ }
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) |