Some Variants of the Weakest Precondition in Nondeterminism

The duality and some variants of weakest precondition in nondeterminism are discussed, namely weakest possible precondition, strongly-deterministic precondition, weakest liberal precondition and non-terminating precondition. The duality of weakest precondition makes the construction of these variants of weakest precondition possible. A study of the variants sharpens our intuition about nondeterminism. It turns out that, contrary to the usual belief, indetermining precondition does not exist.