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) |