Weakest preconditions for progress (Q1189258)

The authors begin their study with an overview of results on predicates and predicate transformers as used in this context. It provides the notation and terminology for the remainder of this paper. Next, they link a predicate transfer for expressing progress properties to an operational interpretation of program execution. This leads to a set of requirements that seem reasonable to expect from any predicate transformer that satisfies the interpretation. The authors define the predicate transformer by induction over the program structure, and they establish some theorems about it. Finally, they repeat these steps for another progress property and its predicate transformer.