Eliminating disjunctions of leads-to properties (Q1318740)

Leads-to properties allow specification of \textit{progress properties} of reactive programs. We define a predicate transformer, in terms of which finite disjunctions of leads-to properties can be rewritten as equivalent single leads-to properties. Although disjunctions of leads-to properties do not typically arise in progress specifications, we give an example showing how they may be introduced through manipulation of nested implications of leads-to properties; such \textit{nested} implications allow subtle dependencies between a program's progress and that of its environment to be conveniently specified. After introducing the predicate transformer we show how to define a single leads-to property equivalent to a given disjunction of two leads-to properties. An equivalent definition in terms of \textit{unless} properties is given. Finally, we generalize the predicate transformer to any finite number of arguments.