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.