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

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