×

Characterizing specification languages which admit initial semantics. (English) Zbl 0536.68011

Summary: The paper proposes an axiomatic approach to specification languages, and introduces notions of reducibility and equivalence as tools for their study and comparison. Algebraic specification languages are characterized up to equivalence. They are shown to be limited in expressive power by implicational languages.

MSC:

68P05 Data structures
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Goguen, J. A.; Thatcher, J.; Wagner, E., Abstract data types as initial algebras and correctness of data representations, (Yeh, R., Current Trends in Programming Methodology, Vol. 4 (1978), Prentice-Hall: Prentice-Hall New York), 80-149
[2] Andreka, H.; Nemeti, I., Generalization of variety and quasivariety concepts to partial algebras through category theory, Dissertationes Math., 204 (1982), (Rozprawy Mat.) · Zbl 0518.08007
[3] Barwise, J.; Feferman, S., Higher Model Theory: Logic of Mathematical Concepts (1983), Springer: Springer Berlin
[4] Burstall, R. M.; Goguen, J. A., The semantics of CLEAR, a specification language, Proc. 1979 Copenhagen Winter School of Abstract Software Specifications (1980) · Zbl 0456.68024
[5] Banaschewski, B.; Herrlich, H., Subcategories defined by implications, Houston J. Math., 2, 2, 149-171 (1976) · Zbl 0344.18002
[6] Bergstra, J. A.; Tucker, J. V., Algebraic specifications of computable and semicomputable data structures, TR IW-115/79 (1979), Mathematisch Centrum: Mathematisch Centrum Amsterdam · Zbl 0419.68029
[7] de Carvalho, R. L.; Maibaum, T. S.E.; Pequeno, T. H.C.; Pereda, A. A.; Veloso, P. A.S., A model theoretic approach to the theory of abstract data types and data structures, Res. Rept. CS-80-22 (1980), Waterloo: Waterloo Ontario
[8] Cudnovskii, G. V., Some results in the theory of infinitely long expressions, Soviet Math. Dokl., 9, 556-559 (1968) · Zbl 0315.02016
[9] Goguen, J. A.; Burstall, R. M., INSTITUTIONS: Abstract model theory for program specification (1982), Draft version · Zbl 0518.68009
[10] Gratzer, G., Universal Algebra (1979), Springer: Springer Berlin · Zbl 0182.34201
[11] Guttag, J. V., The specification and application to programming of abstract data types, TR CSRG-59 (1975), Toronto
[12] Kamin, S., Some definitions for algebraic data types specifications, SIGPLAN Notices, 14, 3 (1979)
[13] Kamin, S., Final data type specifications: A new data type specification method, Proc. 7th POPL-Conference (1980)
[14] Mahr, B.; Makowsky, J. A., An axiomatic approach to semantics of specification languages, (Theoretical Computer Science, 6th Gl-Conf. Dortmund 1983, 145 (1983), Springer: Springer Berlin), 211-219, Lecture Notes in Computer Science · Zbl 0493.68023
[15] Mahr, B.; Makowsky, J. A., Characterizing specification languages which admit initial semantics, (CAAP’83, 159 (1983), Springer: Springer Berlin), 300-316, Lecture Notes in Computer Science · Zbl 0522.68026
[16] Makowsky, J. A., Model theoretic issues in theoretical computer science, Proc. Logic Colloquim’82 (1982), Florence · Zbl 0553.68028
[17] Makowsky, J. A., Compactness, embeddings and definability; and, Abstract embedding relations, Higher Model Theory: Logic of Mathematical Concepts (1983), Springer: Springer Berlin, Chapters 18, 20
[18] Mal’cev, A. I., Quasiprimitive classes of abstract algebras in the metamathematics of algebraic systems, (Studies in Logic, 66 (1971), North-Holland: North-Holland Amsterdam), 27-31
[19] Monk, J. D., Mathematical Logic (1976), Springer: Springer Berlin · Zbl 0354.02002
[20] Selman, A., Completeness of calculi for axiomatically defined classes of algebras, Algebra Universalis, 2, 1, 20-32 (1972) · Zbl 0251.08005
[21] Wand, M., Final algebra semantics and data type extensions, TR65 (1978), Indiana
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.