Rodin User’s Handbook v.2.8: Assignments

3.3.8 Assignments

3.3.8.1 Deterministic Assignments

$\mathrel {:\mkern 1mu=}$

:=

deterministic assignment

Description

$x_1,\ldots ,x_ n \mathrel {:\mkern 1mu=}\textsf{E}_1\ldots ,\textsf{E}_ n$ assigns the expressions $\textsf{E}_ i$ to the variable $x_ i$ , with $i\in 1\mathbin {.\mkern 1mu.}n$ . All $x_ i$ 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:
$x(\textsf{F}) \mathrel {:\mkern 1mu=}\textsf{E}$ .

Definition

The before-after-predicate of $x_1,\ldots ,x_ n \mathrel {:\mkern 1mu=}\textsf{E}_1,\ldots ,\textsf{E}_ n$ is
$x_1’ = \textsf{E}_1 \land \ldots \land x_ n’ = \textsf{E}_ n$ .

This assignment is equivalent to $x_1,\ldots ,x_ n \mathrel {:\mkern 1mu\mid }x_1’ = \textsf{E}_1 \land \ldots \land x_ n’ = \textsf{E}_ n$ .

The special form for this assignment is:
$x(\textsf{F}) \mathrel {:\mkern 1mu=}\textsf{E}\quad \mathrel {\widehat=}\quad x \mathrel {:\mkern 1mu=}x \mathbin {\lhd \mkern -9mu-}\{ ~ \textsf{F}\mapsto \textsf{E}~ \}$

Types

$x_ i$ and $E_ i$ must have the same type: $x_ i\in \alpha _ i$ and $\textsf{E}_ i\in \alpha _ i$ for $i \in 1\mathbin {.\mkern 1mu.}n$ .

WD

$\mathcal{L}(~ x_1,\ldots ,x_ n \mathrel {:\mkern 1mu=}\textsf{E}_1,\ldots ,\textsf{E}_ n~ ) \quad \mathrel {\widehat=}\quad \mathcal{L}(\textsf{E}_1) \land \ldots \land \mathcal{L}(\textsf{E}_ n)$
$\mathcal{L}(~ x(\textsf{F}) \mathrel {:\mkern 1mu=}\textsf{E}~ ) \quad \mathrel {\widehat=}\quad \mathcal{L}(\textsf{F}) \land \mathcal{L}(\textsf{E})$

3.3.8.2 Non-deterministic assignment with before-after-predicate

$\mathrel {:\mkern 1mu\mid }$

:|

non-deterministic assignment with a before-after-predicate

Description

$x_1,\ldots ,x_ n \mathrel {:\mkern 1mu\mid }Q$ assigns any value to the variables $x_1\ldots ,x_ n$ such that the the before-after-predicate $Q$ is fulfilled. Each $x_ i$ is an identifier that refers to a variable of the concrete machine.

All free identifiers in $Q$ must be constants, concrete parameters, concrete variables or primed versions of the modified variables ( $x_1’,\ldots ,x_ n’$ ).

This is the most general form of assignment. All other assignments can be converted to this.

Definition

The before-after-predicate is $Q$ .

Types

$Q$ is a predicate and all $x_ i$ and $x’_ i$ must have the same type: $x_1\in \alpha _ i$ and $x’_1\in \alpha _ i$ for $i\in 1\mathbin {.\mkern 1mu.}n$ .

WD

$\mathcal{L}(~ x_1,\ldots ,x_ n \mathrel {:\mkern 1mu\mid }Q~ ) \quad \mathrel {\widehat=}\quad \forall x_1’,\ldots ,x_ n’ \mathord {\mkern 1mu\cdot \mkern 1mu}\mathcal{L}(~ Q~ )$

Feasibility

$\mathcal{F}(~ x_1,\ldots ,x_ n \mathrel {:\mkern 1mu\mid }Q(x_1’,\ldots ,x_ n’)~ )$
$\quad \mathrel {\widehat=}\quad$ $\exists x_1’,\ldots ,x_ n’ ~ \mathord {\mkern 1mu\cdot \mkern 1mu}~ Q(x_1’,\ldots ,x_ n’)$

3.3.8.3 Non-deterministic assignment by sets

$\mathrel {:\mkern 1mu\in }$

::

non-deterministic assignment of a set member

Description

$x \mathrel {:\mkern 1mu\in }\textsf{E}$ assigns any value of the set $\textsf{E}$ to the variable $x$ . $x$ is an identifier that refers to a variable of the concrete machine.