Specification-Driven Design with Eiffel and Agents for Teaching Lightweight Formal Methods

  • Richard F. Paige
  • Jonathan S. Ostroff
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3294)


We report on our experiences in teaching lightweight formal methods with Eiffel. In particular, we discuss how we introduce formal methods via Eiffel’s design-by-contract and agent technologies, and how we integrate these techniques with test-driven development, in an approach called specification-driven design. This approach demonstrates how formal methods techniques fit with industrial software engineering practice.


Software Engineering Formal Method Class Diagram Unit Test Interaction Diagram 
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. 1.
    Ambler, S.: Extreme Testing. Software Development 11(5) (June 2003)Google Scholar
  2. 2.
    Ambler, S.: Agility for Executives. Software Development (September 2003)Google Scholar
  3. 3.
    Beck, K.: Test-driven Development: by example. Addison-Wesley, Reading (2003)Google Scholar
  4. 4.
    Beck, K., Cockburn, A., Jeffries, R., Highsmith, J.: Agile Manifesto (2001),
  5. 5.
    Berry, D.: Formal methods: the very idea – some thoughts about why they work when they work. Science of Computer Programming 42(1) (2002)Google Scholar
  6. 6.
    Boehm, B.W., Turner, R.: Balancing Agility and Discipline: a guide for the perplexed. Addison-Wesley, Reading (2003)Google Scholar
  7. 7.
    Cater, H.: Strategic Command 2, web site at (last accessed June 2004)
  8. 8.
    Hehner, E.C.R.: A Practical Theory of Programming, 2nd edn. Prentice-Hall, Englewood Cliffs (2003)Google Scholar
  9. 9.
    Jackson, M.: Software Requirements and Specifications. ACM Press, New York (1995)Google Scholar
  10. 10.
    Ostroff, J.S., Paige, R.F., Makalsky, D., Brooke, P.J.: ETester: an Agent-Based Testing Framework for Eiffel (June 2004) (submitted)Google Scholar
  11. 11.
    Meyer, B.: Eiffel: the Language, 2nd edn. Prentice-Hall, Englewood Cliffs (1992)zbMATHGoogle Scholar
  12. 12.
    Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall, Englewood Cliffs (1997)zbMATHGoogle Scholar
  13. 13.
    Ostroff, J.S., Makalsky, D., Paige, R.F.: Agile Specification-Driven Design. In: Proc. Extreme Programming 2004, June 2004. LNCS, Springer, Heidelberg (2004)Google Scholar
  14. 14.
    Paige, R.F., Ostroff, J.S., Brooke, P.J.: A Test-Based Agile Approach to Checking the Consistency of Class and Collaboration Diagrams. In: Proc. UK Software Testing Workshop, University of York (September 2003)Google Scholar
  15. 15.
    Paige, R.F., Ostroff, J.S.: ERC: an Object-Oriented Refinement Calculus for Eiffel. Formal Aspects of Computing 16(1), 51–79 (2004)zbMATHCrossRefGoogle Scholar
  16. 16.
    Zave, P., Jackson, M.: Four dark corners of requirements engineering. ACM Transactions on Software Engineering and Methodology 6(1) (1997)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Richard F. Paige
    • 1
  • Jonathan S. Ostroff
    • 2
  1. 1.Department of Computer ScienceUniversity of YorkUK
  2. 2.Department of Computer ScienceYork UniversityCanada

Personalised recommendations