×

zbMATH — the first resource for mathematics

Algebraic specifications of computable and semicomputable data types. (English) Zbl 0637.68013
The authors of this paper are well known contributors in the theory of the abstract data types. This paper is an extensive survey of various specification mechanisms based on initial algebra semantics. The mathematical basis of the algebraic approach to data type specification is reviewed. A proper mathematical analysis and classification of the algebraic specification methods are given. The equational and conditional equational specifications, with and without hidden functions or hidden sorts are described.
Reviewer: G.Grigas

MSC:
68N01 General topics in the theory of software
68Q60 Specification and verification (program logics, model checking, etc.)
68Q55 Semantics in the theory of computing
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Bergstra, J.A.; Broy, M.; Wirsing, M.; Tucker, J.V., On the power of algebraic specifications, (), 193-204, Strbske Pleso, Czechoslovakia · Zbl 0462.68001
[2] Bergstra, J.A.; Ch Meyer, J.-J., On specifying sets of integers, Elektron. informationsverarb. kybernet., 20, 531-541, (1984) · Zbl 0554.68008
[3] Bergstra, J.A.; Tucker, J.V., On the adequacy of finite equational methods for data type specifications, ACM-sigplan notices, 14, 11, 13-18, (1979)
[4] Bergstra, J.A.; Tucker, J.V., Algebraic specifications of computable and semicomputable data structures, () · Zbl 0419.68029
[5] Bergstra, J.A.; Tucker, J.V., A characterisation of computable data types by means of a finite, equational specification method, (), 76-90, Noordwijkerhout, 1980 · Zbl 0449.68003
[6] Bergstra, J.A.; Tucker, J.V., Equational specifications for computable data types: six hidden functions suffice and other sufficiency bounds, () · Zbl 0418.68019
[7] Bergstra, J.A.; Tucker, J.V., On bounds for the specification of finite data types by means of equations and conditional equations, () · Zbl 0421.68020
[8] Bergstra, J.A.; Tucker, J.V., A natural data type with a finite equational final semantics specification but no effective equational initial semantics specification, Bulletin EATCS, 11, 23-33, (1980) · Zbl 0421.68021
[9] Bergstra, J.A.; Tucker, J.V., Algebraically specified programming systems and Hoare’s logic, (), 348-362, Acre, 1981 · Zbl 0465.68003
[10] Bergstra, J.A.; Tucker, J.V., Initial and final algebra semantics for data type specifications: two characterisation theorems, SIAM J. comput., 12, 366-387, (1983) · Zbl 0515.68016
[11] Bergstra, J.A.; Tucker, J.V., The completeness of the algebraic specification methods for data types, Inform. and control, 54, 186-200, (1982) · Zbl 0513.68017
[12] Bergstra, J.A.; Tucker, J.V., Expressiveness and the completeness of Hoare’s logic, J. comput. system sci., 25, 267-284, (1982) · Zbl 0549.68021
[13] Bergstra, J.A.; Tucker, J.V., The axiomatic semantics of programs based on Hoare’s logic, Acta inform., 21, 293-320, (1984) · Zbl 0551.68016
[14] Broy, M.; Dosch, W.; Parsch, H.; Pepper, P.; Wirsing, M., Existential quantifiers in abstract data types, (), 72-87, Graz, 1980
[15] Broy, M.; Wirsing, M., Partial abstract types, Acta inform., 18, 47-64, (1982) · Zbl 0494.68020
[16] Cohn, P.M., Universal algebra, (1965), Harper and Row New York · Zbl 0141.01002
[17] Goguen, J.A.; Thatcher, J.W.; Wagner, E.G.; Wright, J.B., Abstract data types as initial algebras and correctness of data representations, Proc. ACM conference on computer graphics, pattern recognition and data structure, 89-93, (1975), New York
[18] Goguen, J.A.; Thatcher, J.W.; Wagner, E.G., An initial algebra approach to the specification, correctness and implementation of abstract data types, (), 80-149
[19] Grätzer, G., Universal algebra, (1968), Van Nostrand Princeton · Zbl 0182.34201
[20] ()
[21] Guttag, J.V., The specification and application to programming of abstract data types, () · Zbl 0395.68020
[22] Guttag, J.V.; Horning, J.J., The algebraic specification of abstract data types, Acta inform., 10, 27-52, (1978) · Zbl 0369.68010
[23] Heering, J., Partial evaluation and ω-completeness of algebraic specifications, Theoret. comput. sci., 43, 149-167, (1986) · Zbl 0606.68017
[24] Hilfinger, P.N., Correspondence from members, ACM-sigplan notices, 13, 11-12, (1978)
[25] Hoare, C.A.R., An axiomatic basis for computer programming, Comm. ACM, 12, 576-583, (1969) · Zbl 0179.23105
[26] Hoare, C.A.R., Proof of correctness of data representations, Acta inform., 1, 271-281, (1972) · Zbl 0244.68009
[27] Hoare, C.A.R., Notes on data structuring, () · Zbl 0566.68020
[28] Jones, D.W., A note on some limits of the algebraic specification methods, ACM-sigplan notices, 13, 64-67, (1978)
[29] Kutzler, B.; Lichtenberger, F., Bibliography on abstract data types, (1983), Springer Berlin · Zbl 0509.68014
[30] Kamin, S., Some definitions for algebraic data type specifications, ACM-sigplan notices, 14, 28-37, (1979)
[31] Kapur, D., Specifications of majster’s traversable stack and Veloso’s traversable stack, ACM-sigplan notices, 14, 46-53, (1979)
[32] Klaeren, H., A constructive method for abstract algebraic software specification, Theoret. comput. sci., 30, 139-204, (1984) · Zbl 0544.68016
[33] Lallement, G., Semigroups and combinatorial applications, (1978), Wiley New York
[34] Liskov, B.; Zilles, S., Specification techniques for data abstractions, IEEE trans. software engrg., SE-1, 7-19, (1975)
[35] Loeckx, J., Algorithmic specifications of data types, (), 129-147, Acre, 1980
[36] Lyndon, R; Schupp, P., Combinatorial group theory, (1977), Springer Berlin · Zbl 0368.20023
[37] Majster, M.E., Limits of the “algebraic” specification of abstract data types, ACM-sigplan notices, 12, 37-42, (1977) · Zbl 0348.68026
[38] Majster, M.E., Data types, abstract data types and their specification problem, theoret. comput. sci., 8, 89-127, (1979) · Zbl 0393.68022
[39] Mal’cev, A.I., Constructive algebras I, Russian math. surveys, 16, 77-129, (1961) · Zbl 0129.25903
[40] Mal’cev, A.I., Algorithms and recursive functions, (1970), Wolters-Noordhoff Groningen · Zbl 0198.02501
[41] Mal’cev, A.I., Algebraic systems, (1973), Springer Berlin
[42] Meseguer, J.; Goguen, J., Initiality, induction and computability, () · Zbl 0571.68004
[43] Parnas, D.L., On the criteria to be used in decomposing systems into modules, Comm. ACM, 15, 1053-1058, (1972)
[44] Parnas, D.L., A technique for software module specification with examples, Comm. ACM, 15, 330-336, (1972)
[45] Prachar, K., Primzahlverteilung, (1957), Springer Berlin · Zbl 0080.25901
[46] Rabin, M.O., Computable algebra, general theory and the theory of computable fields, Trans. amer. math. soc., 98, 341-360, (1960) · Zbl 0156.01201
[47] Rogers, H., Theory of recursive functions and effective computability, (1967), McGraw-Hill New York · Zbl 0183.01401
[48] Rotman, J.J., Theory of groups, (1973), Allyn and Bacon Boston · Zbl 0262.20001
[49] Subrahmanyam, P.A., On a finite axiomatisation of the data type L, ACM-sigplan notices, 13, 80-84, (1978)
[50] V. Stoltenberg-Hansen and J.V. Tucker, Computable algebra. An introduction to computable rings and fields, in preparation. · Zbl 0944.03040
[51] Thatcher, J.W.; Wagner, E.G.; Wright, J.B., Specification of abstract data types using conditional axioms, IBM research rept. RC 6214, (1979), Yorktown Heights, NY
[52] Thatcher, J.W.; Wagner, E.G.; Wright, J.B., Data type specifications: parametrization and the power of specification techniques, IBM research rept. RC 7757, (1979), Yorktown Heights, NY · Zbl 0495.68020
[53] J.V. Tucker and J.I. Zucker, Program correctness over abstract data types, with error-state semantics, Research Monograph, in preparation. · Zbl 0641.68028
[54] Veloso, P.A.S., Traversable stack with fewer errors, ACM-sigplan notices, 14, 55-59, (1979)
[55] Wand, M., Final algebra semantics and data type extensions, J. comput. system sci., 19, 27-44, (1979) · Zbl 0418.68020
[56] Wirsing, M.; Broy, M., Abstract data types as lattices of finitely generated models, (), Rydzyna, 1980 · Zbl 0441.68014
[57] van Wijngaarden, A., Numerical analysis as an independent science, Bit, 6, 66-81, (1966) · Zbl 0161.12004
[58] Zilles, S., An introduction to data algebras, (1975), IBM Research Laboratory San José, CA, Working Paper
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.