Weakest preconditions for progress
Johan J. Lukkien, Jan L. A. Snepscheut · Formal Aspects of Computing · 1992
Abstract Predicate transformers that map the postcondition and all intermediate conditions of a command to a precondition are introduced. They can be used to specify certain progress properties of sequential programs.