Some Properties of Predicate Transformers
C. A. R. Hoare · Journal of the ACM · 1978
This paper defines some "weakest precondltmn'" predicate transformers, Investigates their "healthiness" properties, and apphes them to Dljkstra's language of guarded commands It shows that Dljkstra's w~ function is not the weakest healthy one, but it ~s clearly the best one for practical programming, because it proves the absence of bhnd alleys from a nondetermmlsac program KEY WORDS AND PHRASES.formal language defimtlon, axmmatlc approach to programming, weakest precondmons, predicate transformers, healthiness condmons, nondetermlnacy, guarded commands, blind alleys, program traces, complementary language definitions CR CATEGORIES 4 20, 5 23, 5 24 General