3 ms·
One sees this with Dijkstra’s guarded commands (which are heavily influenced by Hoare) as well. The conditional and loop both pick some true guard nondeterminis
by User23 4y ago
One sees this with Dijkstra’s guarded commands (which are heavily influenced by Hoare) as well. The conditional and loop both pick some true guard nondeterministically. It’s nice on account of it keeps the theory cleaner and of course trying the cases deterministically in program order in the implementation is fully compatible with the formal nondeterministic semantics.
- 082349872349872 4y agoI used to feel it was tragic that even languages which start with unordered choice tend to migrate to ordered choice under practitioner pressure (and I'm unaware of any language which has gone in the opposite direction). However, now I've made my peace with "working up to isomorphism", and regard ordered choice just as the popular way to specify a state space partition that may also be expressed with (more dignity[0] via) unordered choice. "How I learned to stop worrying and love IF THEN" [0] and perhaps even —if we take a moment to remember EWD— without prematurely making decisions that need not be taken... Edit: wow! we apparently owe the fatbar, ⌷, to some bikeshedding from Knuth... cf p.11 of https://www.cs.utexas.edu/users/EWD/ewd03xx/EWD398.PDF https://www.cs.utexas.edu/users/EWD/ewd03xx/EWD398.PDF