It is easy to see that in the Hoare calculus presented above, non termination can only come from the rule of iteration. Analogously, non termination of a PDL program can only come from the use of the unbounded iteration. The expression Δα indicates that α* can diverge, and this is just the kind of notion we need. We can now inductively define a predicate ∞ such that for a program α, the formula ∞(α) will be true exactly when α can enter a non-terminating computation.