Program Transition

program-proofing

Definition

Program Transition

A program transition is a relation that describes a single computation step of a program. It maps a non-final program configuration to its successor configuration.

Formally, the transition relation is

$$\Rightarrow \subseteq (\underset{\text{non-final}}{\underbrace{\mathcal{L}(\mathrm{Program})\times \mathcal{S}}})\times \mathcal{C},$$

where the left-hand side is a non-final configuration and the right-hand side is either a final or a non-final configuration.

Determinism

Deterministic

Definition

Deterministic Program Transition

A deterministic program transition is a program transition relation in which every non-final program configuration has at most one successor configuration.

Formally, for every non-final configuration $c$, if

$$c\Rightarrow c_1\text{and}c\Rightarrow c_2,$$

then $c_1=c_2$.

Link to original

Nondeterministic

Definition

Nondeterministic Program Transition

An noneterministic program transition is a program transition relation in which some non-final program configurations may have more than one successor configuration.

Formally, there exists a non-final configuration $c$ such that

$$c\Rightarrow c_1\text{and}c\Rightarrow c_2$$

for distinct configurations $c_1\ne c_2$.

Link to original

Examples

Skip

The skip statement leaves the state unchanged.

$$(\text{skip},\sigma )\Rightarrow \sigma$$

Abort

The abort statement has no successor configuration.

$$(\text{abort},\sigma )\nRightarrow \dots$$

Sequencing

If the first command takes one step, then the whole sequence takes one step by advancing to the second command.

$$\frac{(\Pi ,\sigma )\Rightarrow {\sigma }^{\prime }}{(\Pi ;\Omega ,\sigma )\Rightarrow (\Omega ,{\sigma }^{\prime })}$$

This is a typical rule of deterministic program transition in small-step operational semantics.

$$\frac{(\Pi ,\sigma )\Rightarrow ({\Pi }^{\prime },{\sigma }^{\prime })}{(\Pi ;\Omega ,\sigma )\Rightarrow ({\Pi }^{\prime };\Omega ,{\sigma }^{\prime })}$$

If $(\Pi ,\sigma )$ takes one step to $({\Pi }^{\prime },{\sigma }^{\prime })$, then $(\Pi ;\Omega ,\sigma )$ takes one step to $({\Pi }^{\prime };\Omega ,{\sigma }^{\prime })$.

Conditional

For the conditional, the executed branch depends on the value of $e$ in the current state.

$$\frac{[e]\sigma \ne 0}{(\text{if }e\text{ then }\Pi \text{ else }\Omega \text{ fi},\sigma )\Rightarrow (\Pi ,\sigma )}$$ $$\frac{[e]\sigma =0}{(\text{if }e\text{ then }\Pi \text{ else }\Omega \text{ fi},\sigma )\Rightarrow (\Omega ,\sigma )}$$

While

If the condition is false, the loop does nothing.

$$\frac{[e]\sigma =0}{(\text{while }e\text{ do }\Pi \text{ od},\sigma )\Rightarrow \sigma }$$

Otherwise, execute the body once and continue with the loop.

$$\frac{[e]\sigma \ne 0}{(\text{while }e\text{ do }\Pi \text{ od},\sigma )\Rightarrow (\Pi ;\text{while }e\text{ do }\Pi \text{ od},\sigma )}$$

Assignment

An assignment updates only the assigned variable and keeps all other variables unchanged.

$$(v:=e,\sigma )\Rightarrow {\sigma }^{\prime }$$

where

$${\sigma }^{\prime }(w)=\{\begin{array}{ll}[e]\sigma & \text{if }w=v\\ \sigma (w)& \text{if }w\ne v\end{array}$$