Nondeterministic Program Transition

program-proofing

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$.