A Reuse-Oriented Framework for Hierarchical Specifications

  • Sophie Coudert
  • Pascale Le Gall
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1816)


In order to facilitate the reuse of possibly complex hierar-chical specification components, we propose a unified view of them as (generalised) open terms generated by constructors : the atomic modules (for example enrichments or presentations). Thus, all kinds of pieces of specifications are handled in a uniform way. Moreover, they are autonomous in the sense that they are well defined independently from the context of their design. We present an equational axiomatisation of the structure, providing the class of hierarchical specifications with two combination operators. We show on the example of proofs how thanks to this approach, an attribute for a specification may be systematically inherited from the ones of its modules. The so obtained attributes are naturally structured following the specifications.


formal structured specification reuse proof system structured inference typed equational logic monoid language theory 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BCLG96]
    G. Bernot, S. Coudert, and P. Le Gall. Towards heterogeneous formal specifications. In AMAST’96, Munich, pages 458–472. LNCS 1101, 1996.Google Scholar
  2. [BG80]
    R. Burstall and J. Goguen. The semantics of CLEAR, a specification language. In Proc. Advanced Course on Abstract Software Specifications, Berlin, pages 292–332. Springer, 1980.Google Scholar
  3. [BHK90]
    J.A. Bergstra, R. Heering, and P. Klint. Module algebra. Journal of the Association for Computer Machinery, 37(2):335–372, 1990.zbMATHMathSciNetGoogle Scholar
  4. [Bor97]
    T. Borzyszkowski. Correctness of a logical system for structured specifications. In WADT’97, Tarquinia, Italy, pages 107–121. LNCS 1376, 1997.Google Scholar
  5. [BST99]
    M. Bidoit, D. Sannella, and A. Tarlecki. Architectural specification in CASL. In AMAST’98, Amazonia-Manaus, pages 263–277, LNCS 1548, 1999.Google Scholar
  6. [CBLG98]
    S. Coudert, G. Bernot, and P. Le Gall. Hierachical heterogeneous specifications. In WADT’98, Lisbon, Portugal. LNCS 1589, p. 107–121, 1998.Google Scholar
  7. [CM97]
    M. Cerioli and J. Meseguer. May I borrow your logic? Transporting Logical Structures along Maps. TCS, 173(2):311–347, 1997.zbMATHCrossRefMathSciNetGoogle Scholar
  8. [Cou98]
    S. Coudert. Cadre de spécifications hétérogènes. PhDThesis, Universitè d’Évry, France, 1998.Google Scholar
  9. [DGS93]
    R. Diaconescu, J. Goguen, and P. Stefaneas. Logical support for modularisation. In G. Huet and G. Plotkin, editors, Proc. Workshop on Types and Logical Frameworks, p. 83–130, 1993.Google Scholar
  10. [EM85]
    H. Ehrig and B. Mahr. Fundamentals of algebraic specification 1. equations and initial semantics. EATCS Monographs on Theoretical Computer Science, 6, 1985.Google Scholar
  11. [GB92]
    J.A. Goguen and R.M. Burstall. Institutions: Abstract model theory for specification and programming. Journal of ACM, 39(1):95–146, 1992.zbMATHCrossRefMathSciNetGoogle Scholar
  12. [HST94]
    R. Harper, D. Sannella, and A. Tarlecki. Structured theory presentations and logic representations. Annals of Pure and Applied Logic, 67, 1994.Google Scholar
  13. [Mos97]
    P. Mosses. CoFI: The common framework initiative for algebraic specification and development. In Springer, editor, Proc. TAPSOFT’97, Theory and Practice of Software Development, volume 1214, pages 115–137, 1997.Google Scholar
  14. [NOS95]
    M. Navarro, F. Orejas, and A. Sanchez. On the correctness of modular systems. Theoretical Computer Science, 140:139–177, 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  15. [SW83]
    D. Sannella and M. Wirsing. A kernel language for algebraic specifications and implementation. In Proc. FCT’83. LNCS 158, p. 413–427, 1983.Google Scholar
  16. [Wir93]
    M. Wirsing. Structured specifications: syntax, semantics and proof calculus. In Brauer W. Bauer F. and Schwichtenberg H., editors, Logic and Algebra of Specification, pages 411–442. Springer, 1993.Google Scholar
  17. [Wir94]
    M. Wirsing. Algebraic specification languages: An overview. In WADT’94, S. Margherita, Italy, volume 906, pages 81–116. LNCS, 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Sophie Coudert
    • 1
  • Pascale Le Gall
    • 2
  1. 1.LSRSaint Martin d’Heres CedexFrance
  2. 2.L.a.M.I.Université d’ÉvryÉvryFrance

Personalised recommendations