Rutger M. Dijkstra, Beverly A. Sanders: A Predicate Transformer for the Progress Property 'To-Always'. Formal Aspects Comput. 9(3): 270-282 (1997)