Trace Specifications: Methodology and Models

Precise abstract software specification is achievable by using formal specification languages. However, nontrivial specifications are inordinately difficult to read and write. This paper summarizes the trace specification language and presents the trace specification methodology: a set of heuristics designed to make the reading and writing of complex specifications manageable. Also described is a technique for constructing formal, executable models from specifications written using the methodology. These models are useful as proofs of specification consistency and as executable prototypes. Fully worked examples of the methodology and the model building technique are included.