Empty Program (Hoare Calculus)

hoare-calculus

Definition

Empty Program (Hoare Calculus)

The empty program skip does nothing. It leaves the program state unchanged.

In Hoare notation, this means:

$$\{F\}\mathbf{skip}\{F\}{}_{\text{(skip)}}$$