Abstract
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.
Original language | English (US) |
---|---|
Pages (from-to) | 1243-1252 |
Number of pages | 10 |
Journal | IEEE Transactions on Software Engineering |
Volume | 14 |
Issue number | 9 |
DOIs | |
State | Published - Sep 1988 |
Externally published | Yes |
Keywords
- Formal specification
- logic
- prototype
- software engineering
ASJC Scopus subject areas
- Software