User Manual for Rodin v.2.3: Assignments

3.3.8 Assignments

We did not consider the scope of the expressions in the previous sections, i.e. we did not say which constants or variables can be used in an expression or predicate because this depends completely on the context where the expression is used.

The following paragraphs are about assignments. Depending on the type of assignment it may be important to specify which identifiers can be used. Thus we use the notion $E(x_1,\ldots ,x_ n)$ to specify which free identifiers may occur in the expression $E$ .

3.3.8.1 Deterministic Assignments

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

:=

deterministic assignment

Description

$x_1,\ldots ,x_ n \mathrel {:\mkern 1mu=},E_{1}(\mathbf{c},\mathbf{w},\mathbf{u})\ldots ,E_{n}(\mathbf{c},\mathbf{w},\mathbf{u})$ assigns the expressions $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. $\mathbf{c},\mathbf{w},\mathbf{u}$ represent the sequence of all constants, variables of the concrete machine and parameters of the concrete event.

There is a special form of the assignment which does a relational overwrite:
$x(F(\mathbf{c},\mathbf{w},\mathbf{u})) \mathrel {:\mkern 1mu=}E(\mathbf{c},\mathbf{w},\mathbf{u})$ .

Definition

The before-after-predicate of $x_1,\ldots ,x_ n \mathrel {:\mkern 1mu=}E_{1}(\mathbf{c},\mathbf{w},\mathbf{u}),\ldots ,E_{n}(\mathbf{c},\mathbf{w},\mathbf{u})$ is
$x_1’ = E_{1}(\mathbf{c},\mathbf{w},\mathbf{u}) \land \ldots \land x_ n’ = E_{n}(\mathbf{c},\mathbf{w},\mathbf{u})$ .

The assignment is equivalent to $x_1,\ldots ,x_ n \mathrel {:\mkern 1mu\mid }x_1’ = E_{1}(\mathbf{c},\mathbf{w},\mathbf{u}) \land \ldots \land x_ n’ = E_{n}(\mathbf{c},\mathbf{w},\mathbf{u})$ .

The special form is syntactic sugar for:
$x(E_{1}(\mathbf{c},\mathbf{w},\mathbf{u})) \mathrel {:\mkern 1mu=}E_{2}(\mathbf{c},\mathbf{w},\mathbf{u}) \quad \mathrel {\widehat=}\quad x \mathrel {:\mkern 1mu=}x \mathbin {\lhd \mkern -9mu-}\{ ~ E_{1}(\mathbf{c},\mathbf{w},\mathbf{u}) \mapsto E_{2}(\mathbf{c},\mathbf{w},\mathbf{u})~ \}$

Types

$x_ i\in \alpha$ and $E_{i}(\mathbf{c},\mathbf{w},\mathbf{u})\in \alpha$ for $i \in 1\mathbin {.\mkern 1mu.}n$ .

WD

$\mathcal{L}(~ x_1,\ldots ,x_ n \mathrel {:\mkern 1mu=}E_{1}(\mathbf{c},\mathbf{w},\mathbf{u}),\ldots ,E_{n}(\mathbf{c},\mathbf{w},\mathbf{u})~ ) \quad \mathrel {\widehat=}\quad \mathcal{L}(E_{1}(\mathbf{c},\mathbf{w},\mathbf{u})) \land \ldots \land \mathcal{L}(E_{n}(\mathbf{c},\mathbf{w},\mathbf{u}))$
$\mathcal{L}(~ x(E_{1}(\mathbf{c},\mathbf{w},\mathbf{u})) \mathrel {:\mkern 1mu=}E_{2}(\mathbf{c},\mathbf{w},\mathbf{u})~ ) \quad \mathrel {\widehat=}\quad \mathcal{L}(E_{1}(\mathbf{c},\mathbf{w},\mathbf{u})) \land \mathcal{L}(E_{2}(\mathbf{c},\mathbf{w},\mathbf{u}))$

3.3.8.2 Non-deterministic assignments

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

:|

non-deterministic assignment with a before-after-predicate

Description

$x_1,\ldots ,x_ n \mathrel {:\mkern 1mu\mid }Q(\mathbf{c},\mathbf{w},\mathbf{u},x_1’,\ldots ,x_ n’)$ assigns to the variables $x_1\ldots ,x_ n$ any value such that the the before-after-predicate $Q$ is fulfilled. All $x_ i$ are identifier that refer to a variable of the concrete machine. $\mathbf{c},\mathbf{w},\mathbf{u}$ represent the sequence of all constants, variables of the concrete machine and parameters of the concrete event. $x_1,\ldots ,x_ n$ are in $\mathbf{w}$ .

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

Definition

The before-after-predicate is $Q(\mathbf{c},\mathbf{w},\mathbf{u},x_1’,\ldots ,x_ n’)$ .

Types

$x\in \alpha$ and $E_{}(\mathbf{c},\mathbf{w},\mathbf{u})\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$

WD

$\mathcal{L}(~ x_1,\ldots ,x_ n \mathrel {:\mkern 1mu\mid }Q(\mathbf{c},\mathbf{w},\mathbf{u},x_1’,\ldots ,x_ n’)~ ) \quad \mathrel {\widehat=}\quad \mathcal{L}(x_1,\ldots ,x_ n \mathrel {:\mkern 1mu\mid }Q(\mathbf{c},\mathbf{w},\mathbf{u},x_1’,\ldots ,x_ n’))$

Feasibility

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

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

::

non-deterministic assignment of a set member

Description: $x \mathrel {:\mkern 1mu\in }E_{}(\mathbf{c},\mathbf{w},\mathbf{u})$ assigns to the variable $x$ any value of the set $E$ . $x$ is an identifier that refers to a variable of the concrete machine. $\mathbf{c},\mathbf{w},\mathbf{u}$ represent the sequence of all constants, variables of the concrete machine and parameters of the concrete event.
Definition: The before-after-predicate is $x’ \in E_{}(\mathbf{c},\mathbf{w},\mathbf{u})$ .
The assignment is equivalent to $x \mathrel {:\mkern 1mu\mid }x’ \in E_{}(\mathbf{c},\mathbf{w},\mathbf{u})$ .
Types: $x\in \alpha$ and $E_{}(\mathbf{c},\mathbf{w},\mathbf{u})\in \mathop {\mathbb P\hbox{}}\nolimits (\alpha )$
WD: $\mathcal{L}(~ x \mathrel {:\mkern 1mu\in }E_{}(\mathbf{c},\mathbf{w},\mathbf{u})~ ) \quad \mathrel {\widehat=}\quad \mathcal{L}(E(\mathbf{c},\mathbf{w},\mathbf{u}))$
Feasibility: $\mathcal{F}(~ x \mathrel {:\mkern 1mu\in }E_{}(\mathbf{c},\mathbf{w},\mathbf{u})~ ) \mathrel {\widehat=}E_{}(\mathbf{c},\mathbf{w},\mathbf{u})\neq \emptyset$

Rodin Handbook

3.3.8 Assignments

3.3.8.1 Deterministic Assignments

3.3.8.2 Non-deterministic assignments