A weaker precondition for loops : (preprint)
H.J. Boom · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1978
The purpose of this note is to argue that, contrary to Dijkstra's-Unbounded nondeterminism can be a meaningful programming tool, Its usefulness does not require the existence of infinitely nondeterministic hardware, and -Dijkstra's technical difficulties with unbounded nondeterminism lie with the loop axiom, and not with nondeterminism per se.In fact, a small change in his loop axiom will give unbounded nondeterminism.The new axiom is proved correct using constructive logic with bar induction.