×
Broy, M.; Wirsing, M.; Pair, C.

A systematic study of models of abstract data types. (English) Zbl 0552.68010

Theor. Comput. Sci. 33, 139-174 (1984).
The term-generated models of an abstract data type can be represented by congruence relations on the term algebra. Total and partial heterogeneous algebras are considered as models of hierarchical abstract data types. Particular classes of models are studied and it is investigated under which conditions they form a complete lattice. This theory allows also to describe programming languages (and their semantic models) by abstract types. As example we present a simple deterministic stream processing language.

Cited in 9 Documents

MSC:

68P05 Data structures

Keywords:

abstract data type; Total and partial heterogeneous algebras
Cite Review PDF
Full Text: DOI

References:

[1] Thatcher, J. W.; Wagner, E. G.; Wright, J. B., Specification of abstract data types using conditional axioms, IBM Res. Rept. RC-6214 (1976) · Zbl 0333.93002
[2] Goguen, J. A.; Thatcher, J. W.; Wagner, E. G., An initial algebra approach to the specification, correctness and implementation of abstract data types, (Yeh, R., Current Trends in Programming Methodology IV: Data Structuring (1978), Prentice-Hall: Prentice-Hall Englewood Cliffs, NJ), 80-144
[3] Wagner, E. G.; Thatcher, J. W.; Wright, J. B., Programming Languages as mathematical objects, (7th MFCS. 7th MFCS, Lecture Notes in Computer Science, 64 (1978), Springer: Springer Berlin) · Zbl 0394.68008
[4] Thatcher, J. W.; Wagner, E. G.; Wright, J. B., More on advice on structuring compilers and proving their correctness, (Maurer, H. A., Proc. 6th Colloquium on Automata, Languages and Programming. Proc. 6th Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, 71 (1979), Springer: Springer Berlin), 596-615 · Zbl 0412.68013
[5] Andreka, H.; Burmeister, B.; Nemeti, I., Quasivarieties of partial algebras—a unifying approach towards a two-valued model theory for partial algebras, (Preprint Nr. 557 (1980), FB Mathematik: FB Mathematik TH Darmstadt) · Zbl 0537.08004
[6] Bergstra, J. A.; Broy, M.; Tucker, J. B.; Wirsing, M., On the power of algebraic specifications, (10th MFCS. 10th MFCS, Lecture Notes in Computer Science, 118 (1981), Springer: Springer Berlin), 193-204 · Zbl 0462.68001
[7] Bertoni, A.; Mauri, G.; Miglioli, P. A., A characterisation of abstract data types as model-theoretic invariants, (Maurer, H. A., Proc. 6th Colloquium on Automata, Languages and Programming. Proc. 6th Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, 71 (1979), Springer: Springer Berlin), 26-27 · Zbl 0411.68033
[8] Broy, M.; Wirsing, M., Algebraic definition of a functional programming language, (TUM 18008 (1980), TU München, Institut für Informatik). (TUM 18008 (1980), TU München, Institut für Informatik), R.A.I.R.O. Informatique Theorique, 17, 2, 137-161 (1983), Revised version · Zbl 0515.68017
[9] Broy, M.; Wirsing, M., Programming languages as abstract data types, (5ème Coll. Les Arbres en Algèbre et Programmation (1980), Lille), 160-177, Lille · Zbl 0433.68014
[10] Broy, M.; Wirsing, M., Partial recursive functions and abstract data types, EATCS Bulletin, 11, 34-41 (1980) · Zbl 0433.68014
[11] Broy, M.; Wirsing, M., Partial abstract types, Acta Informatica, 18, 1, 47-64 (1982), Revised version · Zbl 0494.68020
[12] Broy, M.; Wirsing, M., Generalized heterogeneous algebras, (Ausiello, G.; Protasi, M., 8th Coll. on Trees and Algebra in Programming. 8th Coll. on Trees and Algebra in Programming, Lecture Notes in Computer Science, 159 (1983), Springer: Springer New York), 1-34 · Zbl 0522.08001
[13] Broy, M.; Dosch, W.; Partsch, H.; Pepper, P.; Wirsing, M., Existential quantifiers in abstract data types, (Maurer, H. A., Proc. 6th Colloquium on Automata, Languages and Programming. Proc. 6th Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, 71 (1979), Springer: Springer Berlin), 73-87 · Zbl 0404.68026
[14] Burstall, R. M.; Goguen, J. A., An informal introduction to specifications using Clear, (Boyer, R.; Moore, J., The Correctness Problem in Computer Science (1981), Academic Press: Academic Press New York) · Zbl 0518.68009
[15] Bauer, F. L.; Broy, M.; Dosch, W.; Krieg-Brückner, B.; Laut, A.; Luckmann, M.; Matzner, T.; Möller, B.; Partsch, H.; Pepper, P.; Samelson, K.; Steinbrüggen, R.; Wirsing, M.; Wössner, H., Programming in a wide spectrum language: A collection of examples, Sci. Comput. Programm., 1, 1, 73-114 (1981) · Zbl 0469.68003
[16] Liskov, B.; Snydes, A.; Atkinson, R.; Schaffert, C., Abstraction mechanism in CLU, Comm. ACM, 20, 546-576 (1977) · Zbl 0362.68018
[17] Dosch, W.; Wirsing, M.; Ausiello, G.; Mascari, G. F., Polynomials—the specification, analysis and development of an abstract data type, (Wilhelm, R., GI-10 Jahrestagung Saarbrücken. GI-10 Jahrestagung Saarbrücken, Informatik Fachbericht, 33 (1980), Springer: Springer Berlin), 306-320
[18] Gaudel, M. C., Génération et preuve de compilateurs basées sur une sémantique formelle des langages de programmation, Thèse d’Etat (1980), Nancy
[19] Giarratana, V.; Gimona, F.; Montanari, U., Observability concepts in abstract data type specifications, (5th MFCS. 5th MFCS, Lecture Notes in Computer Science, 45 (1976), Springer: Springer Berlin), 576-587 · Zbl 0338.68023
[20] Goguen, J. A., Abstract errors for abstract data types, Proc. IFIP Working Conf. on Formal Description of Programming Language Concepts, 1977. Proc. IFIP Working Conf. on Formal Description of Programming Language Concepts, 1977, UCLA Semantics and Theory of Computation Report, 46 (1977) · Zbl 0373.68024
[21] Goguen, J. A.; Meseguer, J., Completeness of many-sorted equational logic, SIGPLAN Notices, 16, 7, 24-32 (1981) · Zbl 0498.03018
[22] Grätzer, H., Universal Algebra (1968), Van Nostrand: Van Nostrand Princeton · Zbl 0182.34201
[23] Guttag, J. V., The specification and application to programming of abstract data types, (Ph.D. Thesis (1975), University of Toronto) · Zbl 0395.68020
[24] Guttag, J. V.; Horning, J. J., The algebraic specification of abstract data types, Acta Informatica, 10, 27-52 (1978) · Zbl 0369.68010
[25] Guttag, J. V., Notes on type abstraction, (Bauer, F. L.; Broy, M., Program Construction. Program Construction, Lecture Notes in Computer Science, 69 (1979), Springer: Springer Berlin), 593-616 · Zbl 0399.68031
[26] Horn, A., On sentences which are true of direct unions of algebras, J. Symbolic Logic, 16, 14-21 (1951) · Zbl 0043.24801
[27] Huet, G., Confluent reductions: abstract properties and applications to term rewriting systems, 18th IEEE Symp. on Foundations of Computer Science, 30-45 (1977)
[28] Huet, G.; Oppen, D., Equations and rewrite rules: A survey, (Book, R., Formal Languages: Perspectives and Open Problems (1980), Academic Press: Academic Press New York)
[29] Hussmann, H., Operativitätskriterien für algebraische Typen, (Diplomarbeit (1983), Technische Universität München, Institut für Informatik)
[30] Kamin, S., Some definitions for algebraic data type specifications, SIGPLAN Notices, 14, 3, 28-37 (1979)
[31] Knuth, D.; Bendix, P., Simple word problems in abstract algebras, (Leech, Computational Problems in Abstract Algebras (1970), Pergamon: Pergamon Oxford), 263-297 · Zbl 0188.04902
[32] Milner, R., Fully abstract models of typed λ-calculi, Theoret. Comput. Sci., 4, 1-22 (1977) · Zbl 0386.03006
[33] Mosses, P., A constructive approach to compiler correctness, (de Bakker, J.; Leeuwen, J.v.d., Proc. 7th Colloquium on Automata, Languages and Programming. Proc. 7th Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, 85 (1979), Springer: Springer Berlin)
[34] Pair, C., Types abstraits et sémantique algébrique des langages de programmation, (Rept. 80-R-011 (1980), Centre de Recherche en Informatique de Nancy) · Zbl 0229.68025
[35] Pair, C., Sur les modèles de types abstraits algébriques, (Rept. 80-P-052 (1980), Centre de Recherche en Informatique de Nancy) · Zbl 0203.26602
[36] Pair, C., Abstract data types and algebraic semantics of programming languages, Theoret. Comput. Sci., 18, 1-13 (1982) · Zbl 0499.68010
[37] Partsch, H.; Broy, M., Examples for change of types and object structures, (Bauer, F. L.; Broy, M., Program Construction. Program Construction, Lecture Notes in Computer Science, 69 (1979), Springer: Springer Berlin), 421-463 · Zbl 0399.68030
[38] Pepper, P., A study on transformational semantics, (Bauer, F. L.; Broy, M., Program Construction. Program Construction, Lecture Notes in Computer Science, 69 (1979), Springer: Springer Berlin), 322-405 · Zbl 0408.68074
[39] Reichel, H., Theorie der Aequoide, (Dissertation (1979), B. Humboldt Universität Berlin)
[40] Schütte, K., Beweistheorie (1960), Springer: Springer Berlin · Zbl 0102.24704
[41] Scott, D., Continuous lattices, (Proc. 1971 Dalhousie Conf.. Proc. 1971 Dalhousie Conf., Lecture Notes Mathematics, 274 (1971), Springer: Springer Berlin), 97-136 · Zbl 0239.54006
[42] Wand, M., First order identities as a defining language, (Tech. Rept. 29 (1977), Indiana University, Computer Science Department). (Tech. Rept. 29 (1977), Indiana University, Computer Science Department), Acta Informatica, 14, 337-357 (1980), see also · Zbl 0424.68022
[43] Wand, M., Final algebra semantics and data type extensions, (Tech. Rept. 65 (1978), Indiana University). (Tech. Rept. 65 (1978), Indiana University), J. Comput. Systems Sci., 19, 27-44 (1979), see also · Zbl 0418.68020
[44] Wirsing, M.; Broy, M., Abstract data types as lattices of finitely generated models, (9th MFCS. 9th MFCS, Lecture Notes in Computer Science, 88 (1980), Springer: Springer Berlin), 673-685 · Zbl 0441.68014
[45] Wirsing, M.; Pepper, P.; Partsch, H.; Dosch, W.; Broy, M., On hierarchies of abstract data types, (Tech. Rept. TUM-18007 (1980), TU München). (Tech. Rept. TUM-18007 (1980), TU München), Acta Informatica, 20, 1-33 (1983), revised version · Zbl 0513.68015
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.