Safe Object-Oriented Software: The Verified Design-By-Contract Paradigm

  • David Crocker


In recent years, large sectors of the software development industry have moved from the procedural style of software development to an object-oriented style. Safety-critical software developers have largely resisted this trend because of concerns about verifiability of object-oriented systems. This paper outlines the benefits offered by object technology and considers the key features of the object-oriented approach from a user’s perspective. We review the main issues affecting safety and propose a paradigm — Verified Design-by-Contract — that uses formal methods to facilitate the safe use of inheritance, polymorphism, dynamic binding and other features of the object-oriented approach. An outline of Perfect Developer — a tool supporting the Verified Design-by-Contract paradigm — is included.


Unify Modeling Language Verification Condition Object Technology Unify Modeling Language Model Dynamic Binding 
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. Bames J (1997). High Integrity Ada: the SPARK Approach. Addison-Wesley, England.Google Scholar
  2. Chalin P (2003). Improving JML: For a Safer and More Effective Language. FME 2003: Formal Methods (Springer LNCS 2805): 440.Google Scholar
  3. Flanagan C, Leino K.R.M, Lillibridge M, Nelson C, Saxe J and Stata R (2002). Extended static checking for Java. Proc. PLDI, SIGPLAN Notices 37 (5): 234–245.CrossRefGoogle Scholar
  4. Hoare C.A.R (1969). An axiomatic basis for computer programming, Communications of the ACM 12: 576–580.MATHCrossRefGoogle Scholar
  5. Jones Rand Lins R (1996). Garbage Collection. Wiley, England.MATHGoogle Scholar
  6. Kramer R (1998). iContract - The Java(tm) Design by Contract(tm) Tool. Technology of Object-Oriented Languages and Systems, August 03–07: 295.Google Scholar
  7. Mamrak A and Sinha S (1999): A case study: productivity and quality gains using an object-oriented framework. Software - Practice and Experience 29 (6): 501–518.CrossRefGoogle Scholar
  8. Meyer B (1988). Object-Oriented Software Construction. Prentice Hall, England.Google Scholar
  9. Meyer B (1992). Eiffel: The Language. Prentice Hall.MATHGoogle Scholar
  10. OOTiA (2003). Handbook for Object-Oriented Technology in Aviation (draft). OOTiA Workshop Proceedings, March 5, 2003.Google Scholar
  11. Port D and McArthur M (1999). A Study of Productivity and Efficiency for Object-Oriented Methods and Languages. APSEC 1999 (IEEE Computer Society): 128-.Google Scholar
  12. Potok T, Vouk M and Rindos A (1999). Productivity Analysis of Object-Oriented Software Developed in a Commercial Environment. Software - Practice and Experience 29 (10): 833–847.CrossRefGoogle Scholar
  13. RTJ (2003). (30 September 2003).Google Scholar
  14. Warren J.H and Oldman R.D (2003). A Rigorous Specification Technique for High Quality Software, Proceedings of the Twelfth Safety-Critical Systems Symposium, Springer-Verlag (London).Google Scholar

Copyright information

© Springer-Verlag London 2004

Authors and Affiliations

  • David Crocker
    • 1
  1. 1.Escher Technologies Ltd.AldershotUK

Personalised recommendations