Abstract
A new notion is given for the implementation of one specification by another. Unlike most previous notions, this generalises to handle parameterised specifications as well as loose specifications (having an assortment of non-isomorphic models). Examples are given to illustrate the notion. The definition of implementation is based on a new notion of the simulation of a theory by an algebra. For the bulk of the paper we employ a variant of the Clear specification language [BG 77] in which the notion of a data constraint is replaced by the weaker notion of a hierarchy constraint. All results hold for Clear with data constraints as well, but only under more restrictive conditions.
We prove that implementations compose vertically (two successive implementation steps compose to give one large step) and that they compose horizontally under application of (well-behaved) parameterised specifications (separate implementations of the parameterised specification and the actual parameter compose to give an implementation of the application).
The full version of this paper is available as Report CSR-103-82, Department of Computer Science, University of Edinburgh.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bauer, F.L. et al (the CIP Language Group) Report on a wide spectrum language for program specification and development (tentative version). Report TUM-I8104, Technische Univ. München.
Broy, M., Dosch, W., Partsch, H., Pepper, P. and Wirsing, M. Existential quantifiers in abstract data types. Proc. 6th ICALP, Graz, Austria. LNCS 71, PP. 73–87.
Broy, M., Möller, B., Pepper, P. and Wirsing, M. A model-independent approach to implementations of abstract data types. Proc. of the Symp. on Algorithmic Logic and the Programming Language LOGLAN, Poznan, Poland. LNCS (to appear).
Burstall, R.M. and Goguen, J.A. Putting theories together to make specifications. Proc. 5th IJCAI, Cambridge, Massachusetts, pp. 1045–1058.
Burstall, R.M. and Goguen, J.A. The semantics of Clear, a specification language. Proc. of Advanced Course on Abstract Software Specifications, Copenhagen. LNCS 86, pp. 292–332.
Burstall, R.M., MacQueen, D.B. and Sannella, D.T. HOPE: an experimental applicative language. Proc. 1980 LISP Conference, Stanford, California, pp. 136–143; also Report CSR-62-80, Dept. of Computer Science, Univ. of Edinburgh.
Dijkstra, E.W. Notes on structured programming. Notes on Structured Programming (Dahl O.-J., Dijkstra, E.W. and Hoare, C.A.R.), Academic Press, pp. 1–82.
Ehrich, H.-D. On realization and implementation. Proc. 10th MFCS, Strbske Pleso, Czechoslovakia. LNCS 118.
Ehrich, H.-D. On the theory of specification, implementation, and parameterization of abstract data types. JACM 29, 1 pp. 206–227.
Ehrig, H. and Kreowski, H.-J. Parameter passing commutes with implementation of parameterized data types. Proc. 9th ICALP, Aarhus, Denmark (this volume).
Ehrig, H., Kreowski, H.-J. and Padawitz, P. Algebraic implementation of abstract data types: concept, syntax, semantics and correctness. Proc. 7th ICALP, Noordwijkerhout, Netherlands. LNCS 85, pp. 142–156.
Ganzinger, H. Parameterized specifications: parameter passing and implementation. TOPLAS (to appear).
Goguen, J.A. and Burstall, R.M. CAT, a system for the structured elaboration of correct programs from structured specifications. Computer Science Dept., SRI International.
Goguen, J.A., Thatcher, J.W. and Wagner, E.G. An initial algebra approach to the specification, correctness, and implementation of abstract data types. Current Trends in Programming Methodology, Vol. 4: Data Structuring (R.T. Yeh, ed.), Prentice-Hall, pp. 80–149.
Grätzer, G. Universal Algebra (2nd edition), Springer.
Guttag, J.V. and Horning, J.J. The algebraic specification of abstract data types. Acta Informatica 10 pp. 27–52.
Hupbach, U.L. Abstract implementation of abstract data types. Proc. 9th MFCS, Rydzyna, Poland. LNCS 88, pp. 291–304.
Hupbach, U.L. Abstract implementation and parameter substitution. Proc. 3rd Hungarian Computer Science Conference, Budapest.
Kaphengst, H. and Reichel, H. Algebraische Algorithmentheorie. VEB Robotron, Zentrum für Forschung und Technik, Dresden.
MacQueen, D.B. and Sannella, D.T. Completeness of proof systems for equational specifications. In preparation.
Nourani, F. Constructive extension and implementation of abstract data types and algorithms. Ph.D. thesis, Dept. of Computer Science, UCLA.
Reichel, H. Initially-restricting algebraic theories. Proc. 9th MFCS, Rydzyna, Poland. LNCS 88, pp. 504–514.
Sannella, D.T. A new semantics for Clear. Report CSR-79-81, Dept. of Computer Science, Univ. of Edinburgh.
Schoett, O. Ein Modulkonzept in der Theorie Abstrakter Datentypen. Report IFI-HH-B-81/81, Fachbereich Informatik, Universität Hamburg.
Thatcher, J.W., Wagner, E.G. and Wright, J.B. Data type specification: parameterization and the power of specification techniques. SIGACT 10th Annual Symp. on the Theory of Computing, San Diego, California.
Wand, M. Final algebra semantics and data type extensions. JCSS 19 pp. 27–44.
Wirsing, M. and Broy, M. An analysis of semantic models for algebraic specifications. International Summer School on Theoretical Foundations of Programming Methodology, Marktoberdorf.
Wirth, N. Program development by stepwise refinement. CACM 14, 4 pp. 221–227.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1982 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sannella, D., Wirsing, M. (1982). Implementation of parameterised specifications. In: Nielsen, M., Schmidt, E.M. (eds) Automata, Languages and Programming. ICALP 1982. Lecture Notes in Computer Science, vol 140. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0012793
Download citation
DOI: https://doi.org/10.1007/BFb0012793
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-11576-2
Online ISBN: 978-3-540-39308-5
eBook Packages: Springer Book Archive