Leads-to Properties and the But-not-yet Operator.pdf

Leads-to Properties andthe But-not-yet OperatorKen CalvertCollege of ComputingGeorgia Institute of TechnologyAtlanta, Georgia 30032-0280calvert@cc.gatech.eduGIT{CC{93/60October 1993AbstractWe dene a predicate transformer, in terms of which nite disjunctions of leads-toproperties can be rewritten as single leads-to properties. Although disjunctions ofleads-to properties do not typically arise naturally in progress specications, anexample shows how they may be introduced through the use of nested implica-tions of leads-to properties; such implications allow subtle dependencies between aprograms progress and that of its environment to be conveniently specied. Afterintroducing the predicate transformer, which is called the but-not-yet operator,we show how to dene a single leads-to property equivalent to a given disjunctionof two leads-to properties. An alternative denition of the but-not-yet operatoris shown to be equivalent to the rst, and some properties of the operator areproved. Finally, the predicate transformer is generalized to any nite number ofarguments. College of ComputingGeorgia Institute of TechnologyAtlanta, Georgia 30332{0280 1 IntroductionMany specication formalisms use some fragment of linear temporal logic to specify programproperties. In such formalisms, sequences of states represent the possible behaviors of aprogram. A temporal property is a predicate on sequences of states; a program satises such aproperty P if and only if P is true for each sequence representing a possible program behaviors.In recent years it has been demonstrated that a wide range of properties useful in practicecan be specied using a few simple temporal forms [4, 5, 6, 7, 8].This paper considers a class of properties built up from basic temporal properties usingboolean connectives: the temporal predicate P ^Q is true for a sequence i both P and Q are;P _Q is true i either P or Q is, and P ) Q is true i either P is not true or Q is true. Thefamiliar laws of proposit