An approach to abstract specification based on traces
Daniel L. Chester · 2005
This paper presents a formalism for specifying the funct onal properties of abstract data types. This formalism is more powerful than the algebraic formalism of Guttag and others because procedures can be specified as easily as functions. After an explanation of why algebraic specitications are not appropriate for most software development the key concepts of the formalism are explained and illustrated. A format for the specification of an abstract data type is presented. An example of such a specification follows, after which some limits of this approach are discussed.