Promela Reference -- assignment(4)

Google

Promela

BasicStatements

assignment(4)

NAME
assignment statement.

SYNTAX
varref = any_expr
varref ++ as an abbreviation of: varref = varref + 1
varref -- as an abbreviation of: varref = varref - 1

EXECUTABILITY
True

EFFECT
Replaces the value of varref with the integer value of any_expr , where necessary after truncating the value to the range of the declared data type 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 language C, the assignment as a whole returns no value and can therefore itself not be part of an expression.

The reference to a variable, varref , can be an arbitrary scalar, array element, or structure element.

EXAMPLES

a = 12	/* scalar */

r.b[a] = a * 4 + 7	/* structure element */

NOTES
All variables must be declared before they can be referenced in assignments. The default initial value of all variables is zero.

SEE ALSO
datatypes(2), condition(4).


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