|
:= |
deterministic assignment |
assigns the expressions
to the variable
, with
. All
must be distinct identifiers that refer to variables of the concrete machine.
There is a special form of the assignment which uses a relational overwrite:.
The before-after-predicate of is
.
This assignment is equivalent to .
The special form for this assignment is:
and
must have the same type:
and
for
.
|
:| |
non-deterministic assignment with a before-after-predicate |
assigns any value to the variables
such that the the before-after-predicate
is fulfilled. Each
is an identifier that refers to a variable of the concrete machine. We write
to emphasise the fact that the identifiers
can also be used for the constants, concrete variables and parameters in the predicate
.
This is the most general form of assignment. All other assignments can be converted to this.
The before-after-predicate is .
is a predicate and all
and
must have the same type:
and
for
.
|
:: |
non-deterministic assignment of a set member |
assigns any value of the set
to the variable
.
is an identifier that refers to a variable of the concrete machine.
The before-after-predicate is .
The assignment is equivalent to .
and