Formal Methods for Component Software: The Refinement Calculus Perspective

  • Martin Büchi
  • Emil Sekerinski
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1357)


We exhibit the benefits of using formal methods for constructing and documenting component software. Formal specifications provide concise and complete descriptions of black-box components and, herewith, pave the way for full encapsulation. Specifications using abstract statements scale up better than prepostconditions and allow for ‘relative’ specifications because they may refer to other components. Nondeterminism in specifications permits enhancements and alternate implementations. A formally verifiable refinement relationship between specification and implementation of a component ensures compliance with the published specification. Unambiguous and complete contracts are the foundation of any component market.


Abstract Statement Formal Contract Alternate Implementation Complete Contract Future Enhancement 
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.
    Ásgeir Ólafsson and Doug Bryan. On the need for “required interfaces” of components. In M. Mühlhaeuser, editor, Special Issues in Object-Oriented Programming, pages 159–165. dpunkt Verlag Heidelberg, 1997. ISBN 3-920993-67-5.Google Scholar
  2. 2.
    R. J. R. Back and Joackim von Wright. Refinement Calculus: A Systematic Introduction. Springer Verlag, to appear 1997.Google Scholar
  3. 3.
    Richard Helm, Ian M. Holland, and Dipayan Gangopadhyay. Contracts: Specifying behavioral compositions in object-oriented systems. In Proceedings of OOPSLA/ECOOP’ 90 Conference on Object-Oriented Programming Systems, Languages and Application, pages 169–180, October 1990.Google Scholar
  4. 4.
    Jean-Marc Jézéquel and Bertrand Meyer. Put it in the contract: The lessons of ariane. IEEE Computer, pages 129–130, January 1997.Google Scholar
  5. 5.
    W. Kozaczynski and J. O. Ning. Concern-driven design for a specification language. In Proceedings of the 8th International Workshop on Software Specification and Design, Berlin, Germany, March 1996.Google Scholar
  6. 6.
    Bertrand Meyer. Object-Oriented Software Construction. Prentice Hall, second edition, 1997.Google Scholar
  7. 7.
    Oscar Nierstrasz and Dennis Tsichritzis, editors. Object-Oriented Software Composition. Prentice Hall, 1995.Google Scholar
  8. 8.
    David Garlan, Daniel Jackson, Mary Shaw, and Jeannette Wing. Composable software systems, 1996.
  9. 9.
    Clemens A. Szyperski and Cuno Pfister. Component-oriented programming: WCOP’96 workshop report. In M. Mühlhaeuser, editor, Special Issues in Object-Oriented Programming, pages 127–130. dpunkt Verlag Heidelberg, 1997. ISBN 3-920993-67-5.Google Scholar
  10. 10.
    Martin Büchi and Wolfgang Weck. A plea for grey-box components. In Foundations of Component-Based Systems’ 97, 1997.
  11. 11.
    Amy M. Zaremsky and Jeannette M. Wing. Specification matching of software components. In SIGSOFT Foundations of Software Engineering, October 1995. Also CMU-CS-95-127.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Martin Büchi
    • 1
  • Emil Sekerinski
    • 1
  1. 1.Turku Centre for Computer ScienceTurkuFinland

Personalised recommendations