Infinite Program Run

program-proofing

Definition

Infinite Program Run

An infinite program run is a program run that does not terminate.

Formally,

$${\gamma }_0\Rightarrow {\gamma }_1\Rightarrow {\gamma }_2\Rightarrow \cdots$$

with no last configuration.

An infinite run means that the program loops or stays active forever.

Example

While loop

$(\text{while }1\text{ do skip od},\sigma )$

Since $[1]\sigma =1$, we have

$$(\text{while }1\text{ do skip od},\sigma )\Rightarrow (\text{skip};\text{while }1\text{ do skip od},\sigma )$$

and then

$$(\text{skip};\text{while }1\text{ do skip od},\sigma )\Rightarrow (\text{while }1\text{ do skip od},\sigma )$$

so the run repeats forever:

$$(\text{while }1\text{ do skip od},\sigma )\Rightarrow (\text{skip};\text{while }1\text{ do skip od},\sigma )\Rightarrow (\text{while }1\text{ do skip od},\sigma )\Rightarrow \cdots$$