A Rigorous Specification Technique for High Quality Software

  • John H. Warren
  • Robin D. Oldman
Conference paper


Too many software projects fail. One important reason, though not the only one, is the absence of a good specification. Specifications should be complete, consistent, comprehensible, and correct. Correctness can only be demonstrated if the specification is formal (so that reasoning can be supported); but the associated use of a formal language seriously reduces user comprehension, so there is a conflict between these two properties. We contend that formal methods should be used but that their use should be totally concealed and automated, so that users are unaware of the underlying formality. We have constructed a specification toolset, called CREATIV, which embodies this approach.

The use of formal methods mandates a scientific approach. One possible approach is to formalise specification knowledge as an axiomatic system. The CREATIV toolset uses a new model and a new definition of the specification process, together with an axiomatic theory to support specification knowledge. All operations in the system are provable and traceable; we have built the reasoning component of the CREATIV toolset on the basis of this theory.

We have used the toolset for specification on a range of projects. More recently, we have used it on a small number of government projects. We report on some of the advantages of its use, and offer some preliminary comments on a comparative specification exercise.


Formal Method Formal Language Axiomatic System Tile System Reasoning System 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. BCS Review (2001): Scholar
  2. Chaos Report (1994): Scholar
  3. Crocker (2004): “Safe Object-Oriented Software: The Verified Design-by-Contract Paradigm”, D. Crocker, Proceedings of 12th Safety Critical Systems Symposium, Springer-Verlag (London)Google Scholar
  4. Pierce (2002): “Types and Programming Languages”, Benjamin C. Pierce, MIT Press (2002), ISBN 0-262-16209-1 Page xxi, quotation attributed to Tom MelhamGoogle Scholar

Copyright information

© Springer-Verlag London 2004

Authors and Affiliations

  • John H. Warren
    • 1
  • Robin D. Oldman
    • 1
  1. 1.Precision Design Technology Ltd.Maidenhead, BerkshireEngland

Personalised recommendations