Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Towards heterogeneous formal specifications

  • Conference
  • Conference paper
  • First Online:
Algebraic Methodology and Software Technology (AMAST 1996)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1101))

Abstract

We believe that big software systems could be more easily formally specified if several specification approaches were allowed within a single system specification. We propose a notion of heterogeneous framework where the specifier can choose a dedicated specification framework for each specification module. We show how the resulting heterogeneous modular specifications can get semantics, and how modular proofs can still be performed on these specifications. Our contribution is mainly focussed on a sort of interoperability between heterogeneous specification modules and we retrieve, as much as possible, classical notions of “meta-formalisms,” modularity for structured specifications, or inference systems, as they are well known in the algebraic specification community. With this respect, our work can be regarded as an attempt to unify frameworks, by accepting and formalizing heterogeneity.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. E. Astesiano and M. Cerioli. Relationships between logical frameworks. In LNCS, editor, Recent Trends in Data Type Specification, volume 655, pages 101–126, Dourdan, 1992.

    Google Scholar 

  2. G. Bernot and M. Bidoit. Proving the correctness of algebraically specified software modularity and observability issues. In Proc. of AMAST-2, Second Conference of Algebraic Methodology and Software Technology, May 1991. Iowa City, Iowa, USA.

    Google Scholar 

  3. G. Bernot, M. Bidoit, and T. Knapik. Observational approaches to algebraic specifications: A comparative study. Acta Informatica, 31:651–671, 1994.

    Google Scholar 

  4. E.K. Blum, H. Ehrig, and F. Parisi-Pressicce. Algebraic specification of modules and their basic inter-connections. Journal of Computer Systems Science, 34:293–339, 1987.

    Google Scholar 

  5. M. Bidoit, R. Hennicker, and M. Wirsing. Behavioural and abstractor specifications. Science of Computer Programming, 25:149–186, 1995.

    Google Scholar 

  6. M. Barr and C. Wells. Category Theory for Computer Science. Prentice Hall, 1990.

    Google Scholar 

  7. M. Cerioli and J. Meseguer. Can I borrow your logic? In Proc. Int. Mathematical Foundations of Computer Science, MFC'93, Gdansk, pages 342–351, 1993.

    Google Scholar 

  8. S. Coudert. Vers une sémantique des spécifications hétérogènes. Université d'Evry, Rapport de DEA, 1995.

    Google Scholar 

  9. M. Cerioli and G. Reggio. Institutions for very abstract specifications. In LNCS, editor, Recent Trends in Data Type Specification, Caldes de Malavella, volume 785, pages 113–127, 1994.

    Google Scholar 

  10. E. David and C. Roques. An institution for modular specifications. Proc. of the 10th British Colloquium on Theoretical Computer Science, Bristol, 1994.

    Google Scholar 

  11. H. Ehrig and M. Grosse-Rhode. Functorial theory of parameterized specifications in a general specification framework. Theoretical Computer Science, pages 221–266, 1994. Elsevier Science Pub. B.V. (North-Holland).

    Google Scholar 

  12. H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1. Equations and initial semantics, volume 6. Springer-Verlag,EATCS Monographs on Theoretical Computer Science, 1985.

    Google Scholar 

  13. J.A. Goguen and R.M. Burstall. Introducing institutions. In Springer-Verlag LNCS 164, editor, Proc. of the Workshop on Logics of Programming, pages 221–256, 1984.

    Google Scholar 

  14. R. Hennicker. Context induction: a proof principle for behavioural abstractions and algebraic implementations. Formal Aspects of Computing, 3(4):326–345, 1991.

    Google Scholar 

  15. J. Meseguer. General logics. In North-Holland, editor, Proc. Logic. Colloquium '87, Amsterdam, 1989.

    Google Scholar 

  16. S. Mac Lane. Categories for the working mathematician, volume 5 of Graduate texts in mathematics. Springer-Verlag, 1971.

    Google Scholar 

  17. M. Navarro, F. Orejas, and A. Sanchez. On the correctness of modular systems. Theoretical Computer Science, 140:139–177, 1995.

    Google Scholar 

  18. A. Salibra and G. Scollo. A soft stairway to institutions. In LNCS, editor, Recent Trends in Data Type Specification, volume 655, pages 320–329, Dourdan, 1992.

    Google Scholar 

  19. A. Sernadas and C. Sernadas. Theory spaces. Technical report, IST, Lisboa, 1995.

    Google Scholar 

  20. D. Sannella and A. Tarlecki. Toward formal development of programs from algebraic specifications: Implementations revisited. Acta Informatica, 25:233–281, 1988.

    Google Scholar 

  21. U. Wolter. Institutional frames. In LNCS, editor, Recent Trends in Data Type Specification, volume 906, pages 469–482, 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. L.a.M.I., Université d'Évry, Cours Monseigneur Roméro, 91025, Evry Cedex, France

    Gilles Bernot, Sophie Coudert & Pascale Le Gall

Authors
  1. Gilles Bernot
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sophie Coudert
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Pascale Le Gall
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Martin Wirsing Maurice Nivat

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bernot, G., Coudert, S., Le Gall, P. (1996). Towards heterogeneous formal specifications. In: Wirsing, M., Nivat, M. (eds) Algebraic Methodology and Software Technology. AMAST 1996. Lecture Notes in Computer Science, vol 1101. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014333

Download citation

  • DOI: https://doi.org/10.1007/BFb0014333

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61463-0

  • Online ISBN: 978-3-540-68595-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation