Abstract
In an approach for the implementation of loose abstract data type specifications that completely distinguishes between the syntactical level of specifications and the semantical level of models, vertical implementation composition is defined compatibly on both levels. Implementations have signatures, models, and sentences where the latter also include hidden components, which allows for useful normal form results. We illustrate the stepwise development of implementations as well as their composition by some examples and describe the incorporation of the concept into an integrated software development and verification system.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Bergstra, J.A., Broy, M., Tucker, J.V., Wirsing, M.: On the power of algebraic specifications. Proc. 10th MFCS, LNCS Vol. 118, pp. 193–204, 1981.
Burstall, R.M., Goguen, J.A.: The semantics of Clear, a specification language. Proc. of Advanced Course on Abstract Software Specifications, LNCS Vol.86, pp. 292–332.
Beierle,C., Olthoff, W., Voß, A.: Towards a formalization of the software development process. Proc. Software Engineering '86, Southampton, 1986.
Beierle, C., Voß, A.: Implementation specifications. In: H.-J. Kreowski (ed): Recent Trends in Data Type specifications. Informatik Fachberichte 116, Springer, 1985.
Beierle, C., Voß, A.: Algebraic specifications and implementations in an integrated software development and verification system. Memo SEKI-85-12, FB Informatik, Univ. Kaiserslautern (joint SEKI-Memo containing the Ph.D. thesis by Ch. Beierle and the Ph.D. thesis by A. Voß), Dec. 1985.
Ehrich, H.-D.: On the theory of specification, Implementation and Parametrization of Abstract Data Types. JACM Vol. 29, No. 1, Jan. 1982, pp. 206–227.
Ehrig, H.: Algebraic Theory of Parameterized Specifications with Requirements. Proc. 6th Colloquium on Trees in Algebra and Programming (E. Astesiano, C. Böhm, eds.), LNCS 112, pp. 1–24, 1981.
Ehrig, H., Kreowski, H.-J., Mahr, B., Padawitz, P.: Algebraic Implementation of Abstract Data Types. Theor. Computer Science Vol. 20, 1982, pp. 209–254.
Ehrig, H., Wagner, E., Thatcher, J.: Algebraic Constraints for specifications and canonical form results. Draft version, TU Berlin, June 1982.
Ganzinger, H.: Parameterized Specifications: Parameter Passing and Implementation with respect to Observability. ACM TOPLAS Vol. 5, No.3, July 1983, pp. 318–354.
Goguen, J.A., Burstall, R.M.: Institutions: Abstract Model Theory for Program Specification. SRI International and University of Edinburgh, 1983, revised 1985.
Goguen, J.A., Meseguer, J.: Universal Realization, Persistent Interconnection and Implementation of Abstract Modules. Proc. 9th ICALP, LNCS 140, 1982, pp. 265–281.
Goguen, J.A., Thatcher, J.W., Wagner, E.G.: An initial algebra approach to the specification, correctness, and implementation of abstract data types, in: Current Trends in Programming Methodology, Vol.4, Data Structuring (ed. R. Yeh), Prentice-Hall, 1978, pp. 80–144.
Hupbach, U.L.: Abstract implementation of abstract data types. Proc. 9th MFLS, Rydzyna, Poland. LNCS, Vol. 88, pp. 291–304, 1980.
Hupbach, U.L., Kaphengst, H., Reichel, H.: Initial algebraic specifications of data types, parameterized data types, and algorithms. VEB Robotron, Zentrum für Forschung und Technik, Dresden, 1980.
Lipeck, U.: Ein algebraischer Kalkül für einen strukturierten Entwurf von Datenabstraktionen. Dissertation. Bericht Nr. 148, Universität Dortmund, 1983.
Schoett, O.: A theory of program modules, their specification and implementation. Draft report, Univ. of Edinburgh, 1982.
Sannella, D.T., Wirsing, M.: Implementation of parameterized specifications, Proc. 9th ICALP 1982, LNCS Vol. 140, pp 473–488.
Sannella, D., Wirsing, M.: A kernel language for algebraic specification and implementation. Proc. FCT, LNCS Vol. 158, 1983.
Thatcher, J.W., Wagner, E.G., Wright, J.B.: Data Type Specification: Parameterization and the Power of Specification Techniques. ACM TOPLAS Vol. 4, No. 4, Oct. 1982, pp. 711–732.
Urbassek, C.: Ein Implementierungskonzept für ASPIK-Spezifikationen und Korrektheitskriterien. Diploma thesis, Univ. Kaiserslautern, 1985.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1987 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Beierle, C., Voß, A. (1987). On implementations of loose abstract data type specifications and their vertical composition. In: Brandenburg, F.J., Vidal-Naquet, G., Wirsing, M. (eds) STACS 87. STACS 1987. Lecture Notes in Computer Science, vol 247. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0039610
Download citation
DOI: https://doi.org/10.1007/BFb0039610
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-17219-2
Online ISBN: 978-3-540-47419-7
eBook Packages: Springer Book Archive