Program Configuration

program-proofing

Definition

Program Configuration

A program configuration is a snapshot of a running program. It consists of the remaining program to be executed together with the current program state.

Formally, a configuration is either a pair $(\Pi ,\sigma )$, where $\Pi \in \mathcal{L}(\mathrm{Program})$ and $\sigma \in \mathcal{S}$, or just a state $\sigma$ in the case of a final configuration.

The set of all configurations is

$$\mathcal{C}\stackrel{\mathrm{def}}{=}(\underset{\text{non-final}}{\underbrace{\mathcal{L}(\mathrm{Program})\times \mathcal{S}}})\cup \underset{\text{final}}{\underbrace{\mathcal{S}}}$$

Program Counter

A program configuration records, among other things, the part of the program that still remains to be executed. This is closely related to the program counter, which points to the current instruction or control position in the program.