A Comparison of Led-from and Leads-to
Edgar Knapp · 1988
Progress properties of parallel programs are often expressed using the operator leads-to, a binary relation over predicates on the program state. Informally, p leads-to q means that from a state satisfying p a state satisfying q is reached eventually. We investigate the notion of the weakest predicate that leads-to q, for some given q. We formalize this notion by defining a predicate transformer called led-from and show that led-from maps a predicate q to the weakest predicate that leads-to q. We also demonstrate that led-from and leads-to are equivalent in expressive power by showing that each can be defined in terms of the other. The advantages of basing concurrent program semantics on the predicate transformer led-from rather than the relation leads-to are similar to those of basing sequential program semantics on the predicate transformer wp rather than on the relation of Hoare-Triples {p}S{q}. In particular, questions about junctivity properties can be raised and answered. Am...