Leads-to Properties and the But-not-yet Operator
Abstract
We define a predicate transformer, in terms of which finite disjunctions of
leads-to properties can be rewritten as single leads-to properties. Although
disjunctions of leads-to properties do not typically arise naturally in
progress specifications, an example shows how they may be introduced through
the use of nested implications of leads-to properties; such implications allow
subtle dependencies between a program's progress and that of its environment
to be conveniently specified.
After introducing the predicate transformer, which is called the "but-not-yet"
operator, we show how to define a single leads-to property equivalent to a
given disjunction of two leads-to properties. An alternative definition of
the but-not-yet operator is shown to be equivalent to the first, and some
properties of the operator are proved. Finally, the predicate transformer is
generalized to any finite number of arguments.