Some Properties of Predicate Transformers

Abstract

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 wp function is not the weakest healthy one, but it is clearly the best one for practical programming, because it proves the absence of bhnd alleys from a nondetermmlsac program. © 1978, ACM. All rights reserved.