Abstract
A kernel specification language called ASL is presented. ASL comprises five fundamental but powerful specification-building operations and has a simple semantics. Behavioural abstraction with respect to a set of observable sorts can be expressed, and (recursive) parameterised specifications can be defined using a more powerful and more expressive parameterisation mechanism than usual. A simple notion of implementation permitting vertical and horizontal composition (i.e. it is transitive and monotonic) is adopted and compared with previous more elaborate notions. A collection of identities is given which can provide a foundation for the development of programs by transformation.
The full version of this paper is available as Report CSR-131-83, Dept. of Computer Science, Univ. of Edinburgh.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
9 References
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 RC6487. Also in: Current Trends in Programming Methodology, Vol. 4: Data Structuring (R.T. Yeh, ed.), Prentice-Hall, pp. 80–149 (1978).
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.
Ehrig, H., Kreowski, H.-J., Thatcher, J.W., Wagner, E.G. and Wright, J.B. Parameterized data types in algebraic specification languages (short version). Proc. 7th ICALP, Noordwijkerhout, Netherlands. LNCS 85, pp. 157–168.
Bauer, F.L. et al (the CIP Language Group) Report on a wide spectrum language for program specification and development (tentative version). Report TUM-18104, Technische Univ. München.
Bauer, F.L. et al (the CIP Language Group) Programming in a wide spectrum language: a collection of examples. Science of Computer Programming 1, pp. 73–114.
Bergstra, J.A., Broy, M., Tucker, J.V. and Wirsing, M. On the power of algebraic specifications. Proc. 10th MFCS, Strbske Pleso, Czechoslovakia. LNCS 118, pp. 193–204.
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.
Bergstra, J.A. and Meyer, J.J. I/O computable data structures. SIGPLAN Notices 16, 4 pp. 27–32.
Ehrich, H.-D. On the theory of specification, implementation, and parametrization of abstract data types. Report 82, Univ. of Dortmund. Also in: JACM 29, 1 pp. 206–227 (1982).
Ehrig, H. and Kreowski, H.-J. (1982) Parameter passing commutes with implementation of parameterized data types. Proc. 9th ICALP, Aarhus, Denmark. LNCS 140, pp. 197–211.
Ehrig, H., Kreowski, H.-J., Mahr, B. and Padawitz, P. Algebraic implementation of abstract data types. Theoretical Computer Science 20, pp. 209–263.
Ehrich, H.-D. and Lipeck, U. Algebraic domain equations. Report 125, Univ. of Dortmund.
Ehrig, H., Thatcher, J.W., Lucas, P. and Zilles, S.N. Denotational and initial algebra semantics of the algebraic specification language LOOK. Draft report, IBM research.
Gaudel, M.-C. Personal communication with M. Wirsing.
Goguen, J.A. and Burstall, R.M. CAT, a system for the structured elaboration of correct programs from structured specifications. Technical report CSL-118, Computer Science Laboratory, SRI International.
Goguen, J.A. and Burstall, R.M. Institutions: logic and specification. Draft report, SRI International.
Giarratana, V., Gimona, F. and Montanari, U. Observability concepts in abstract data type specification. Proc. 5th MFCS, Gdansk. LNCS 45, pp. 576–587.
Goguen, J.A. and Meseguer, J. Universal realization, persistent interconnection and implementation of abstract modules. Proc. 9th ICALP, Aarhus, Denmark. LNCS 140, pp. 310–323.
Goguen, J.A. and Meseguer, J. An initiality primer. Draft report, SRI International.
Gordon, M.J., Milner, A.J.R. and Wadsworth, C.P. Edinburgh LCF. LNCS 78.
Guttag, J.V. The specification and application to programming of abstract data types. Ph.D. thesis, Univ. of Toronto.
Hupbach, U.L., Kaphengst, H. and Reichel, H. Initial algebraic specification of data types, parameterized data types, and algorithms. VEB Robotron, Zentrum für Forschung und Technik, Dresden.
Hornung, G. and Raulefs, P. Terminal algebra semantics and retractions for abstract data types. Proc. 7th ICALP, Noordwijkerhout, Netherlands. LNCS 85, pp. 310–323.
Kamin, S. Final data types and their specification. TOPLAS 5, 1 pp. 97–121.
Liskov, B.H. and Berzins, V. An appraisal of program specifications. Computation Structures Group memo 141-1, Laboratory for Computer Science, MIT.
Reichel, H. Behavioural equivalence — a unifying concept for initial and final specification methods. Proc. 3rd Hungarian Computer Science Conf., Budapest, pp. 27–39.
Sannella, D.T. and Burstall, R.M. Structured theories in LCF. Proc. 8th CAAP, L'Aquila, Italy. LNCS, to appear.
Sannella, D.T. and Wirsing, M. Implementation of parameterised specifications. Report CSR-103-82, Dept. of Computer Science, Univ. of Edinburgh; extended abstract in: Proc. 9th ICALP, Aarhus, Denmark. LNCS 140, pp. 473–488.
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.
Schoett, O. A theory of program modules, their specification and implementation. Draft report, Univ. of Edinburgh.
Wand, M. Final algebra semantics and data type extensions. JCSS 19 pp. 27–44.
Wirsing, M. Structured algebraic specifications. Proc. AFCET Symp. on Mathematics for Computer Science, Paris, pp. 93–107.
Zilles, S.N., Lucas, P. and Thatcher, J.W. A look at algebraic specifications. Draft report, IBM research.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1983 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sannella, D., Wirsing, M. (1983). A kernel language for algebraic specification and implementation extended abstract. In: Karpinski, M. (eds) Foundations of Computation Theory. FCT 1983. Lecture Notes in Computer Science, vol 158. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-12689-9_122
Download citation
DOI: https://doi.org/10.1007/3-540-12689-9_122
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-12689-8
Online ISBN: 978-3-540-38682-7
eBook Packages: Springer Book Archive