Part of the Texts in Computer Science book series (TCS)


A specification of the system under development must include a description of the boundary between the system and its environment. This boundary characterizes the interface of the system. The components in a system interact with each other through their interfaces. It is crucial that each interface specification describes precisely the forms of communication that are permitted at the interface, their causes and effects. Understanding the interface of a component should provide insight into the nature of the system being specified. This is particularly important for systems exhibiting similar behavior, with different interfaces.


Specification Language Time Zone Proof Obligation Interface Specification Deduction Rule 
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.


  1. 1.
    Alagar VS, Colagrosso P, Loukas A, Narayanan S, Protopsaltou A (1996) Formal specifications for effective black-box reuse. Technical reports (2 volumes), Department of Computer Science, Concordia University, Montreal, Canada, February 1996 Google Scholar
  2. 2.
    Chen J (1989) The Larch/Generic interface language. SB thesis, Department of Electrical Engineering and Computer Science, Massachusettes Institute of Technology Google Scholar
  3. 3.
    Cheon Y (1991) Larch/Smalltalk: a specification language for Smalltalk. MSc thesis, Department of Computer Science, Iowa State University Google Scholar
  4. 4.
    Colagrosso P (1993) Formal specification of C++ class interfaces for software reuse. M Comp Sci thesis, Department of Computer Science, Concordia University, Montreal, Canada Google Scholar
  5. 5.
    Guaspari D, Marceau C, Polak W (1990) Formal verification of Ada programs. IEEE Trans Softw Eng 16(9):1058–1075 CrossRefGoogle Scholar
  6. 6.
    Guttag JV, Horning JJ (1993) Larch: languages and tools for formal specification. Springer, Berlin MATHCrossRefGoogle Scholar
  7. 7.
    Jones K (1991) LM3: a Larch interface language for Modula-3: a definition and introduction: version 1.0. Technical report 72, DEC/SRC, Digital Equipment Corporation, MA Google Scholar
  8. 8.
    Leavens GT (1997) Larch/C++ reference manual, draft: revision 5.1, February 1997 Google Scholar
  9. 9.
    Leavens GT, Cheon Y (1992) Preliminary design of Larch/C++. In: Martin U, Wing J (eds) Proceedings of the first international workshop on Larch. Workshops in computer science series. Springer, Berlin Google Scholar
  10. 10.
    Rogue Wave (1993) Tools.h++ class library. Version 6.0, Rogue Wave Software Google Scholar
  11. 11.
    Wing J (1983) A two-tiered approach for specifying programs. Technical report TR_299, Massachusetts Institute of Technology, Laboratory for Computer Science Google Scholar
  12. 12.
    Wing J (1987) Writing Larch interface language specifications. ACM Trans Program Lang Syst 9(1):1–24 MathSciNetMATHCrossRefGoogle Scholar
  13. 13.
    Wing J (1990) A specifier’s introduction to formal methods. IEEE Comput 23(9):8–24 CrossRefGoogle Scholar

Copyright information

© Springer-Verlag London Limited 2011

Authors and Affiliations

  1. 1.Dept. Computer Science and Software Eng.Concordia UniversityMontrealCanada
  2. 2.Computer Science DepartmentUniversity of Wisconsin-La CrosseLa CrosseUSA

Personalised recommendations