A predicate transformer approach to semantics of parallel programs
Charanjit S. Jutla, Edgar Knapp, J. R. Rao · 1989
We present an extensional semantics for parallel programs based on predicate transformers.We identify the meaning of a parallel program with three concepts: a set of initial conditions, a predicate transformer, called wlt, characterizing progress properties of the program, and a predicate transformer wsafe concerned with safety aspects.For a given program, these predicate transformers are defined in terms of fixpoints of recursive equations.