Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Mathematical Foundations of Computer Science

MFCS 1996: Mathematical Foundations of Computer Science 1996 pp 114–134Cite as

Mind the gap! Abstract versus concrete models of specifications

  • Invited Papers
  • Conference paper
  • First Online:

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

Abstract

In the theory of algebraic specifications, many-sorted algebras are used to model programs: the representation of data is arbitrary and operations are modelled as ordinary functions. The theory that underlies the formal development of programs from specifications takes advantage of the many useful properties that these models enjoy.

The models that underlie the semantics of programming languages are different. For example, the semantics of Standard ML uses rather concrete models, where data values are represented as closed constructor terms and functions are represented as “closures”. The properties of these models are quite different from those of many-sorted algebras.

This discrepancy brings into question the applicability of the theory of specification and formal program development in the context of a concrete programming language, as has been attempted in the Extended ML framework for the formal development of Standard ML programs. This paper is a preliminary study of the difference between abstract and concrete models of specifications, inspired by the kind of concrete models used in the semantics of Standard ML, in an attempt to determine the consequences of the discrepancy.

This research was supported by the EC-funded COMPASS Basic Research working group and MeDiCiS Scientific Cooperation Network, by EPSRC grants GR/J07303 and GR/H73103 and by an EPSRC Advanced Fellowship.

This research was supported by the EC-funded COMPASS Basic Research working group and MeDiCiS Scientific Cooperation Network, and by EPSRC grant GR/J07303.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J. Bergstra and J. Tucker. Algebraic specifications of computable and semicomputable data types. Theoretical Computer Science 50:137–181 (1987).

    Article  Google Scholar 

  2. M. Bidoit, H.-J. Kreowski, P. Lescanne, F. Orejas and D. Sannella (eds.) Algebraic System Specification and Development: A Survey and Annotated Bibliography. Springer LNCS 501 (1991).

    Google Scholar 

  3. R. Diaconescu, J.A, Goguen and P. Stefaneas. Logical support for modularisation. In: Logical frameworks (G. Huet and G. Plotkin, eds.), 83–130. Cambridge Univ. Press (1993).

    Google Scholar 

  4. H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1: Equations and Initial Semantics. Springer (1985).

    Google Scholar 

  5. J. Goguen and R. Burstall. Institutions: abstract model theory for specification and programming. Journal of the ACM 39:95–146 (1992).

    Article  Google Scholar 

  6. C.A.R. Hoare. Proofs of correctness of data representations. Acta Informatica 1:271–281 (1972).

    Article  Google Scholar 

  7. S. Kahrs, D. Sannella and A. Tarlecki. The definition of Extended ML. Report ECS-LFCS-94-300, Univ. of Edinburgh (1994).

    Google Scholar 

  8. S. Kahrs, D. Sannella and A. Tarlecki. The definition of Extended ML: a gentle introduction. Report ECS-LFCS-95-322, Univ. of Edinburgh (1995). Theoretical Computer Science, to appear (1996).

    Google Scholar 

  9. J. Loeckx, H.-D. Ehrich and M. Wolf. Specifications of Abstract Data Types. Wiley (1996).

    Google Scholar 

  10. A.I. Mal'cev. Constructive algebras I. Russian Mathematical Surveys 16:77–129 (1961). Also in: The Metamathematics of Algebraic Systems. Collected papers 1936–1967 (B. Wells ed.), 148–212. North-Holland (1971).

    Google Scholar 

  11. J. Meseguer. General logic. Logic Colloquium'87 (H.-D. Ebbinghaus et al., eds.), 279–329. North-Holland (1989).

    Google Scholar 

  12. R. Milner, M. Tofte and R. Harper. The Definition of Standard ML. MIT Press (1990).

    Google Scholar 

  13. L. Paulson. ML for the Working Programmer. Cambridge Univ. Press (1991).

    Google Scholar 

  14. M. Rabin. Computable algebra, general theory and theory of computable fields. Trans, of the AMS 95:341–360 (1960).

    Google Scholar 

  15. H. Rogers, Jr. Theory of Recursive Functions and Effective Computability. McGraw-Hill (1967).

    Google Scholar 

  16. G. Rosolini. About modest sets. Intl. Journal of Foundations of Computer Science 1:341–353 (1990).

    Article  Google Scholar 

  17. D. Sannella. Formal program development in Extended ML for the working programmer. Proc. 3rd BCS/FACS Workshop on Refinement, Hursley Park. Springer Workshops in Computing, 99–130 (1991).

    Google Scholar 

  18. D. Sannella, S. Sokolowski and A. Tarlecki. Toward formal development of programs from algebraic specifications: parameterisation revisited. Acta Informatica 29:689–736 (1992).

    Article  Google Scholar 

  19. D. Sannella and A. Tarlecki. Specifications in an arbitrary institution. Information and Computation 76:165–210 (1988).

    Article  Google Scholar 

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

    Article  Google Scholar 

  21. D. Sannella and A. Tarlecki. Toward formal development of ML programs: foundations and methodology. Proc. 3rd Joint Conf. on Theory and Practice of Software Development, Barcelona. Springer LNCS 352, 375–389 (1989).

    Google Scholar 

  22. D. Sannella and A. Tarlecki. Model-theoretic foundations for formal program development: basic concepts and motivation. ICS PAS Report 791, Institute of Computer Science PAS, Warsaw (1995).

    Google Scholar 

  23. D. Sannella and A. Tarlecki. Foundations of Algebraic Specifications and Formal Program Development. Cambridge Univ. Press, to appear (199?).

    Google Scholar 

  24. D. Sannella and M. Wirsing. A kernel language for algebraic specification and implementation. Proc. 1983 Intl. Conf. on Foundations of Computation Theory, Borgholm. Springer LNCS 158, 413–427 (1983).

    Google Scholar 

  25. O. Schoett. Data Abstraction and the Correctness of Modular Programming. Ph.D. thesis; Report CST-42-87, Univ. of Edinburgh (1987).

    Google Scholar 

  26. V. Stoltenberg-Hansen and J. Tucker. Effective algebras. In: Handbook of Logic in Computer Science, Vol. 4 (S. Abramsky, D. Gabbay and T. Maibaum, eds.), 357–526. Oxford Univ. Press (1995).

    Google Scholar 

  27. A. Tarlecki. Moving between logical systems. Recent Trends in Data Type Specifications. 11th Workshop on Specification of Abstract Data Types (M. Haveraaen et al., eds.). Springer LNCS, to appear (1996).

    Google Scholar 

  28. M. Wirsing. Algebraic specification. In: Handbook of Theoretical Computer Science, Vol. B (J. van Leeuwen, ed.), 675–788. North-Holland (1990).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratory for Foundations of Computer Science, Edinburgh University, Edinburgh, Scotland

    Donald Sannella

  2. Institute of Informatics, Warsaw University, Poland

    Andrzej Tarlecki

  3. Institute of Computer Science, Polish Academy of Sciences, Warsaw, Poland

    Andrzej Tarlecki

Authors
  1. Donald Sannella
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrzej Tarlecki
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Wojciech Penczek Andrzej Szałas

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Sannella, D., Tarlecki, A. (1996). Mind the gap! Abstract versus concrete models of specifications. In: Penczek, W., Szałas, A. (eds) Mathematical Foundations of Computer Science 1996. MFCS 1996. Lecture Notes in Computer Science, vol 1113. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61550-4_143

Download citation

  • DOI: https://doi.org/10.1007/3-540-61550-4_143

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-61550-7

  • Online ISBN: 978-3-540-70597-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation