|
:= |
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.
All free identifiers in must be constants, concrete parameters, concrete variables or primed versions of the modified variables (
).
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.
All free identifiers in must be constants, concrete variables or concrete parameters.
The before-after-predicate is .
The assignment is equivalent to .
and