A formal method for the systematic reuse of specification components

  • Rolf Hennicker
  • Martin Wirsing
Part I. Development Models and Reusability
Part of the Lecture Notes in Computer Science book series (LNCS, volume 544)


This paper presents a method for the systematic reuse of formal specifications. The method is described in the framework of the algebraic specification language ASL which allows to build specifications in a modular way. A reusable component consists of a tree of algebraic specifications representing a software module at different levels of abstraction: the root of the tree is understood as the “abstract” requirement or the design specification of a problem, whereas the leaves correspond to different implementations of the root. We propose to construct such components by reusing already existing components based on the following “divide and conquer” principle: a given specification is decomposed into appropriate subspecifications; these are matched with existing components. Then the recomposition of the successful matchings yields automatically a component for the specification we started with.


Reusable Component Abstract Specification Operation Symbol Correct Implementation Result Component 
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. [Bergstra et al. 86]
    J.A. Bergstra, J. Heering, R. Klint: Module algebra. Centre voor Wiskunde en Informatica, Amsterdam, Report CS: R 8617, 1986.Google Scholar
  2. [Breu 89]
    R. Breu: A normal form for structured algebraic specifications. MIP-Bericht 8917, Universität Passau, 1989.Google Scholar
  3. [Burstall, Goguen 77]
    R.M. Burstall, J.A. Goguen: Putting theories together to make specifications. Proc. 5th Internat. Joint Conf. on Artificial Intelligence, Cambridge M.A., 1977, 1045–1058.Google Scholar
  4. [Cardelli et al. 88]
    L. Cardelli, J. Donahue, L. Glassman, M. Jordan, B. Kalsow, G. Nelson: Modula-3 Report. Digital Systems Research Center, Technical Report 31, August 1988.Google Scholar
  5. [Ehrig, Weber 86]
    H. Ehrig, H. Weber: Programming in the large with algebraic module specifications. In: H. J. Kugler (ed.): Information Processing 86. Amsterdam: North_Holland, 675–684, 1986.Google Scholar
  6. [Feijs 89]
    L.M.G. Feijs: The calculus λπ. In: M. Wirsing, J.A. Bergstra (eds.): Algebraic Methods: Theory, Tools and Applications. Springer Lecture Notes in Computer Science 394, 307–330, 1989.Google Scholar
  7. [Futatsugi et al. 85]
    K. Futatsugi, J.A. Goguen, J.P. Jouannaud, J. Meseguer: Principles of OBJ2. In: Proc. 12th ACM Symposium on Principles of Programming Languages, New Orleans, 1985, 52–66.Google Scholar
  8. [Goguen, Burstall 80]
    J.A. Goguen, R.M. Burstall: CAT, a system for the structured elaboration of correct programs from structured specifications. Computer Science Laboratory, SRI International, Technical Report CSL-118, 1980.Google Scholar
  9. [Guttag et al. 85]
    J.V. Guttag, J.J. Horning, J.M. Wing: Larch in five easy pieces. Digital Systems Research Center, Technical Report 5, 1985.Google Scholar
  10. [Matsumoto 84]
    Y. Matsumoto: Some experiences in promoting reusable software. IEEE Trans. Soft. Eng., Vol. SE-10, no. 5, 1984, 502–513.Google Scholar
  11. [Meyer 88]
    B. Meyer: Object-oriented software construction. International Series in Comp. Science (C.A.R. Hoare ed.), Prentice Hall, New York, 1988.Google Scholar
  12. [Sannella, Tarlecki 88]
    D.T. Sannella, A. Tarlecki: Towards formal development of programs from algebraic specifications: implementations revisited. Acta Informatica 25, 1988, 233–281.Google Scholar
  13. [Sannella, Wirsing 83]
    D.T. Sannella, M. Wirsing: A kernel language for algebraic specification and implementation. In: M. Karpinski (ed.): Coll. on Foundations of Computation Theory 11, Sweden, 1983, Lecture Notes in Computer Science 158, Berlin: Springer, 1983, 413–427.Google Scholar
  14. [Wirsing 86]
    M. Wirsing: Structured algebraic specifications: a kernel language. Theoretical Computer Science 42, 1986, 123–249.Google Scholar
  15. [Wirsing 88]
    M. Wirsing: Algebraic description of reusable software components. In: Proc. COMPEURO 88, Computer Society Press of the IEEE, no. 834, 1988, 300–312.Google Scholar
  16. [Wirsing et al. 88]
    M. Wirsing, R. Hennicker, R. Breu: Reusable specification components. In M. Chytil, L. Janiga, V. Koubek (eds.): Proc. Math. Foundations of Comp. Science, Carlsbad, August/September 1988, Lecture Notes in Computer Science 324, Berlin: Springer, 1988, 121–137.Google Scholar
  17. [Wirsing et al. 89]
    M. Wirsing, R. Hennicker, R. Stabl: MENU — an example for the systematic reuse of specifications. In: C. Ghezzi, J. A. McDermid (eds.): Proc. ESEC '89, 2nd European Software Engineering Conference, Warwick, September 1989. Springer Lecture Notes in Computer Science 387, 1989, 20–41.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Rolf Hennicker
    • 1
  • Martin Wirsing
    • 1
  1. 1.Fakultät für Mathematik und InformatikUniversität PassauPassau

Personalised recommendations