Skip to main content
SpringerLink
Log in
Book cover

Category Theory and Computer Programming pp 364–389Cite as

Extended ML: An institution-independent framework for formal program development

  • Part II Research Contributions
  • Chapter
  • First Online:

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

Abstract

The Extended ML specification language provides a framework for the formal stepwise development of modular programs in the Standard ML programming language from specifications. The object of this paper is to equip Extended ML with a semantics which is completely independent of the logical system used to write specifications, building on Goguen and Burstall's work on the notion of an institution as a formalisation of the concept of a logical system. One advantage of this is that it permits freedom in the choice of the logic used in writing specifications; an intriguing side-effect is that it enables Extended ML to be used to develop programs in languages other than Standard ML since we view programs as simply Extended ML specifications which happen to include only “executable” axioms. The semantics of Extended ML is defined in terms of the primitive specification-building operations of the ASL kernel specification language which itself has an institution-independent semantics.

It is not possible to give a semantics for Extended ML in an institutional framework without extending the notion of an institution; the new notion of an institution with syntax is introduced to provide an adequate foundation for this enterprise. An institution with syntax is an institution with three additions: the category of signatures is assumed to form a concrete category; an additional functor is provided which gives concrete syntactic representations of sentences; and a natural transformation associates these concrete objects with the “abstract” sentences they represent. We use the first addition to “lift” certain necessary set-theoretic constructions to the category of signatures, and the other two additions to deal with the low-level semantics of axioms.

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.

6 References

  1. Barwise, K.J. Axioms for abstract model theory. Annals of Math. Logic 7 pp. 221–265.

    Google Scholar 

  2. Bauer, F.L. et al (the CIP Language Group) Report on a wide spectrum language for program specification and development. Report TUM-I8104, Technische Univ. München. See also: The Wide Spectrum Language CIP-L. Springer LNCS 183 (1985).

    Google Scholar 

  3. Broy, M. and Wirsing, M. Partial abstract types. Acta Informatica 18 pp. 47–64.

    Google Scholar 

  4. Burstall, R.M. and Goguen, J.A. The semantics of Clear, a specification language. Proc. of Advanced Course on Abstract Software Specifications, Copenhagen. Springer LNCS 86, pp. 292–332.

    Google Scholar 

  5. Ehrich, H.-D. On the theory of specification, implementation, and parametrization of abstract data types. Report 82, Univ. of Dortmund. Also in: Journal of the Assoc. for Computing Machinery 29 pp. 206–227 (1982).

    Google Scholar 

  6. Ehrig, H., Kreowski, H.-J., Mahr, B. and Padawitz, P. Algebraic implementation of abstract data types. Theoretical Computer Science 20 pp. 209–263.

    Google Scholar 

  7. Goguen, J.A. and Burstall, R.M. CAT, a system for the structured elaboration of correct programs from structured specifications. Technical report CSL-118, SRI International.

    Google Scholar 

  8. Goguen, J.A. and Burstall, R.M. Introducing institutions. Proc. Logics of Programming Workshop (E. Clarke and D. Kozen, eds.), Carnegie-Mellon University. Springer LNCS 164, pp. 221–256.

    Google Scholar 

  9. Goguen, J.A. and Burstall, R.M. A study in the foundations of programming methodology: specifications, institutions, charters and parchments. Proc. Workshop on Category Theory and Computer Programming, Guildford (this volume). Springer LNCS.

    Google Scholar 

  10. Goguen, J.A., Jouannaud, J.-P. and Meseguer, J. Operational semantics for order-sorted algebra. Proc. 12th Intl. Colloq. on Automata, Languages and Programming, Nafplion, Greece. Springer LNCS 194, pp. 221–231.

    Google Scholar 

  11. Goguen, J.A., Thatcher, J.W. and Wagner, E.G. An initial algebra approach to the specification, correctness, and implementation of abstract data types. IBM research report RC 6487. Also in: Current Trends in Programming Methodology, Vol. 4: Data Structuring (R.T. Yeh, ed.), Prentice-Hall, pp. 80–149 (1978).

    Google Scholar 

  12. Guttag, J.V. The specification and application to programming of abstract data types. Ph.D. thesis, Univ. of Toronto.

    Google Scholar 

  13. Luckham, D.C., von Henke, F.W., Krieg-Brückner, B. and Owe, O. Anna: a language for annotating Ada programs (preliminary reference manual). Technical report 84-248, Computer Systems Laboratory, Stanford University.

    Google Scholar 

  14. MacLane, S. Categories for the Working Mathematician. Springer.

    Google Scholar 

  15. MacQueen, D.B. Modules for Standard ML. Polymorphism 2, 2. See also: Proc. 1984 ACM Symp. on LISP and Functional Programming, Austin, Texas, pp. 198–207.

    Google Scholar 

  16. Milner, R.G. The Standard ML core language. Polymorphism 2, 2. See also: A proposal for Standard ML. Proc. 1984 ACM Symp. on LISP and Functional Programming, Austin, Texas, pp. 184–197.

    Google Scholar 

  17. Nakajima, R. and Yuasa, T. (eds.) The IOTA Programming System: A Modular Programming Environment. Springer LNCS 160.

    Google Scholar 

  18. Reichel, H. Behavioural validity of conditional equations in abstract data types. Contributions to General Algebra 3: Proc. of the Vienna Conference. Verlag Hölder-Pichler-Tempsky, pp. 301–324.

    Google Scholar 

  19. Sannella, D.T. and Burstall, R.M. Structured theories in LCF. Proc. 8th Colloq. on Trees in Algebra and Programming, L'Aquila, Italy. Springer LNCS 159, pp. 377–391.

    Google Scholar 

  20. Sannella, D.T. and Tarlecki, A. Program specification and development in Standard ML. Proc. 12th ACM Symp. on Principles of Programming Languages, New Orleans, pp. 67–77.

    Google Scholar 

  21. Sannella, D.T. and Tarlecki, A. On observational equivalence and algebraic specification. Report CSR-172-84, Dept. of Computer Science, Univ. of Edinburgh; to appear in Journal of Computer and Systems Sciences. Extended abstract in: Proc. 10th Colloq. on Trees in Algebra and Programming, Joint Conf. on Theory and Practice of Software Development (TAPSOFT), Berlin. Springer LNCS 185, pp. 308–322.

    Google Scholar 

  22. Sannella, D.T. and Tarlecki, A. Specifications in an arbitrary institution. Report CSR-184-85, Dept. of Computer Science, Univ. of Edinburgh; to appear in Information and Control. See also: Building specifications in an arbitrary institution, Proc. Intl. Symposium on Semantics of Data Types, Sophia-Antiplis. Springer LNCS 173, pp. 337–356 (1984).

    Google Scholar 

  23. Sannella, D.T. and Tarlecki, A. An institution-independent semantics for Extended ML. Research report, Laboratory for Foundations of Computer Science, Dept. of Computer Science, Univ. of Edinburgh (in preparation).

    Google Scholar 

  24. Sannella, D.T. and Wirsing, M. A kernel language for algebraic specification and implementation. Report CSR-131-83, Dept. of Computer Science, Univ. of Edinburgh. Extended abstract in: Proc. Intl. Conf. on Foundations of Computation Theory, Borgholm, Sweden. Springer LNCS 158, pp. 413–427.

    Google Scholar 

  25. Tarlecki, A. Quasi-varieties in abstract algebraic institutions. Report CSR-173-84, Dept. of Computer Science, Univ. of Edinburgh; to appear in Journal of Computer and Systems Sciences.

    Google Scholar 

  26. Tarlecki, A. On the existence of free models in abstract algebraic institutions. Theoretical Computer Science 37 pp. 269–304.

    Google Scholar 

  27. Wirsing, M. Structured algebraic specifications: a kernel language. Habilitation thesis, Technische Univ. München.

    Google Scholar 

  28. Zilles, S.N. Algebraic specification of data types. Computation Structures Group memo 119, Laboratory for Computer Science, MIT.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Artificial Intelligience, University of Edinburgh, UK

    Donald Sannella

  2. Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, UK

    Donald Sannella

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

    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

David Pitt Samson Abramsky Axel Poigné David Rydeheard

Rights and permissions

Reprints and permissions

Copyright information

© 1986 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Sannella, D., Tarlecki, A. (1986). Extended ML: An institution-independent framework for formal program development. In: Pitt, D., Abramsky, S., Poigné, A., Rydeheard, D. (eds) Category Theory and Computer Programming. Lecture Notes in Computer Science, vol 240. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-17162-2_133

Download citation

  • DOI: https://doi.org/10.1007/3-540-17162-2_133

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-17162-1

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation