A predicate transformer for the progress property ‘to-always’
Rutger M. Dijkstra, Beverly A. Sanders · Formal Aspects of Computing · 1997
Abstract The temporal property ‘to-always’ has been proposed for specifying progress properties of concurrent programs. Although the ‘to-always’ properties are a subset of the ‘leads-to’ properties for a given program, ‘to-always’ has more convenient proof rules and in some cases more accurately describes the desired system behavior. In this paper, we give a predicate transformer wta , derive some of its properties, and use it to define ‘to-always’. Proof rules for ‘to-always’ are derived from the properties of wta . We conclude by briefly describing two application areas, nondeterministic data flow networks and self-stabilizing systems where ‘to-always’ properties are useful.