Program State

program-proofing

Definition

Program State

A program state is a variable assignment for the variables of a program. It maps each program variable to its current value.

Formally,

$$\sigma :\mathcal{L}(\mathrm{Var})\to \mathbb{Z}$$

The set of all program states is

$$\mathcal{S}\stackrel{\mathrm{def}}{=}\{\sigma \mid \sigma :\mathcal{L}(\mathrm{Var})\to \mathbb{Z}\}.$$

If a program $\Pi$ transforms a state $\sigma$ into a state ${\sigma }^{\prime }$, we write

$$[\Pi ](\sigma )={\sigma }^{\prime }\text{or}[\Pi ]\sigma ={\sigma }^{\prime }$$