Abstract
The semantics of type definitions, declarations of structured variables, assignment and evaluation is specified algebraically by means of abstract data types. Corresponding proof rules are given which can be used for program verification. Then, a unifying approach to the semantics of type definitions is presented by giving an axiom system for a general algebra of structured objects in which type definitions are represented by equations. The structure of models for the axiom system and the solvability of these equations is discussed.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
deBakker, J.W.: Correctness proofs for assignment statements. Report IW55/76, Mathematisch Centrum, Amsterdam 1976
Cremers, A.-Hibbard, Th.N.: The semantic definition of programming languages in terms of their data spaces. Proc.4.Fachtagung der GI über Programmiersprachen. Fachberichte Informatik, Springer-Verlag, berlin 1976, 1–11
Ehrich, H.-D.: Outline of an algebraic theory of structured objects, in: Proc. 3rd Int.Coll. on Automata, Languages and Programming, ed. by S.Michaelson and R.Milner, Edinburgh University Press 1976, 508–530
Ehrich, H.-D.: An axiomatic approach to information structures, in: Proc. 5th MFOC Symposium, ed. by A. Mazurkiewicz, Lecture Notes in Computer Science 45, Springer-Verlag, Berlin 1976, 277–283
Goguen, J.A.: Correctness and equivalence of data types, in Proc. Conf. on Alg. Systems Theory, Lecture Notes in Computer Science, Springer-Verlag, Berlin 1975
Goguen, J.A.-Thatcher, J.W.-Wagner, E.G.: An initial algebra approach to the specification, correctness, and implementation of abstract data types, to be published in: Current Trends in Programming Methodology 4, ed. by R. Yeh
Goguen, J.A.-Thatcher, J.W.-Wagner, E.G.-Wright, J.B.: Initial algebra semantics and continuous algebras. Journal of the ACM 24(1977), 68–95
Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1(1972), 271–281
Hoare, C.A.R.: Recursive data structures, Stanford Artificial Intelligence Laboratory Memo AIM-223, STAN-CS-73-400, 1973
Lohberger, V.: Eine Klasse geordneter Monoide und ihre Anwendbarkeit in der Fixpunktsemantik, in: Proc.3rd GI Conf. on Theoretical Computer Science, ed. by H. Tschach, H. Waldschmidt and H.K.-G. Walter, Lecture Notes in Computer Science 48, Springer-Verlag, Berlin 1977, 169–183
Luckham, D.-Suzuki, N.: Automatic program verification V: Verification-oriented proof rules for arrays, records and pointers. Report No. STAN-CS-76-549, Stanford 1976
Spitzen, J.-Wegbreit, B.: The verification and synthesis of data structures, Acta Informatica 4 (1975), 127–144
Standish, Th.A.: Data structures, an axiomatic approach. BBN Report No. 2639, Automatic Programming Memo 3, Bolt Beranek and Newman, Cambridge, Mass. 1973
Wand, M.: First-order identities as a defining language. Tech. Report No. 29, Comp.Sc.Dpt. Indiana University, Bloomington 1976
Wegbreit, B.-Spitzen, J.M.: Proving properties of complex data structures. Journal of the ACM 23(1976), 389–396
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1977 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ehrich, H.D. (1977). Algebraic semantics of type definitions and structured variables. In: Karpiński, M. (eds) Fundamentals of Computation Theory. FCT 1977. Lecture Notes in Computer Science, vol 56. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-08442-8_74
Download citation
DOI: https://doi.org/10.1007/3-540-08442-8_74
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-08442-6
Online ISBN: 978-3-540-37084-0
eBook Packages: Springer Book Archive