Abstract
Our goal is to obtain a specification of a relational data base as an abstract data type in such a way that a computer program can simulate on a small scale the intended use of the data base by generating formal consequences of the specification (that is, without the existence of any implementation of the data base). There are two candidates for the specification formalism to be used: equations and the Horn clauses of logic.
Apart from a specification of a relational data base, the paper is devoted entirely to a comparison between equations and clauses. We compare three aspects: mathematical semantics, the computational aspect, and expressiveness. We propose to discard equations as a distinct formalism, but will regard them as a special case of clauses. In principle we use as specification a clausal sentence containing literally the equations conventionally used in data type specification, but we find certain slight departures conducive to clarity. As program (to be executed by a PROLOG processor) we use another sentence obtained from the specification by a translation process that guarantees correctness.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
ADA: Ichbiah, J.D., Barnes, J.G.P., Heliard, J.C., Krieg-Brueckner, B., Roubine, O., Wichmann, B.A. [1979] Preliminary ADA Reference Manual and Rationale for the Design of the ADA Programming Language, SIGPLAN Notices 14, 6 (June 1979).
ADJ — Goguen, J.A., Thatcher, J.W., Wagner, E.G., and Wright, J.B. [1978] “An Initital Algebra Approach to the Specification, Correctness, and Implementation of Abstract Data Types,” In: Current Trends in Programming Methodology 4 (R. T. Yeh, Ed.), Prentice-Hall, 1978, 80–149.
de Carvalho, R.L., Maibaum, T.S.E., Pequeno, T.H.C., Pereda Borquez, A.A., and Veloso, P.A.S. [1979] “A Model-Theoretic Approach to the Semantics of Data Types and Structures,” Technical Report, DI-PUC/RJ, Rio De Janeiro, Brazil, 1979.
Clark, K. L., and Tärnlund [1977] “A First-Order Theory of Data and Programs,” Proc. IFIP 1977, 939–944.
Colombetti, M., Paolini, P., and Pelagatti, G. [1978] “Non-deterministic Languages Used for the Definition of Data Models”, In: Logic and Data Bases (H. Gallaire and J. Minker, Eds.) Plenum Press, 1978, 237–257.
Courcelle, B. [1979] “Infinite Trees in Normal Form and Recursive Equations Having a Unique Solution,” Technical Report 7906, U.E.R. de mathematique et informatique U. de Bordeaux I, 1979.
van Emden, M.H. and Kowalski, R.A. [1976] “The Semantics of Predicate Logic as a Programming Language,” J. ACM 23 (1976), 733–742.
Goguen, J.A. [1977] “Abstract Errors for Abstract Data Types,” Proc. of IFIP Working Conference on Formal Description of Programming Concepts, North-Holland, 1977.
Goguen, J. A. [1978] “Some Design Principles and Theory for OBJ-O, A Language to Express and Execute Algebraic Specifications of Programs” Proc. of International Conference on Mathematical Studies of Information Processing, Kyoto, 1978, 429–475.
Gotlieb, C. C. and Gotlieb, L. R. [1978] Data Types and Structures, Prentice-Hall, 1978.
Guttag, J. V. [1977] “Abstract Data Types and the Development of Data Structures,” CACM 20, 6 (1977), 396–404.
Guttag, J. and Horning, J. J. [1980]. “Formal Specification as a Design Tool,” In: 7th Annual Sump. on Principles of Programming Languages, 1980, 251–261
Hoare, C.A.R. [1972] “Proof of Correctness of Data Representa-tionsV” Acta Informatica 1, 1 (1972), 271–281.
Hoffman, C., and O’Donnell, M. [1979] “Interpreter Generation Using Tree Pattern Matching” 6th Annual Symp. on Principles of Programming Languages (1979) 169–179.
Huet, G. [1977] “Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems,” Proc. of the 18th IEEE Symp. on Foundations of Computer Science, Providence (1977) 30–45.
Huet, G., and Lankford, D. [1978] “On the Uniform Halting Problem for Term Rewriting Systems,” IRIA Laboria Report 283, 1978.
Kowalski, R. A. [1979] Logic for Problem-Solving, North-Holland, New York (1979).
Kowalski, R. A. and Kuehner, D. [1971] “Linear Resolution with Selection Function,” Artificial Intelligence 2, 227–260.
Lampson, B.W. et al. [1977] “Report on the Programming Language Euclid,” SIGPLAN Notices 12, #2 (Feb. 1977).
Levy, M. R. [1978a] “Verification of Programs with Data Referencing”, Proc. of 3 me Colloque International sur la Programmation, Dunod (1978) 411–426.
Levy, M. R. [1978b] Data Types with Sharing and Circularity, Ph.D. Thesis, Dept. of Comp. Sci., U. of Waterloo, 1978. (Technical Report CS-78–26)
Liskov, B., Snyder, A., Atkinson, R., and Schaffert, C. [1977] “Abstraction Mechanisms in CLU”, CACM 20, 8 (1977), 564–576.
Liskov, B. H., and Zilles, S. N. [1975] “Specification Techniques for Data Abstractions,” IEEE TSE, SE-1, No. 1, 1975, 7–18.
Lockemann, P. C., and Wohlleber, W. H. [1979] “Constraints and Transactions: Extensions to the Algebraic Specification Method,” Technical Report, University of Karlsruhe, 1979.
Maibaum, T.S.E. [1979b] “Data Base Instances, Abstract Data Types and Data Base Specifications.”
Nivat, M. [1973] “On the Interpretation of Recursive Polyadic Program Schemes,” Atti dei Convegno d’Informatica Teorica, Rome, 1973.
O’Donnell, M. J. [1977] “Computing in Systems Described by Equations,” Lecture Notes in Computer Science 58, Springer-Verlag, 1977.
Rosen, B. K. [1973] “Tree-Manipulating Systems and Church-Rosser Theorems,” J. ACM 20 (1973), 160–187.
Shaw, M., Wulf, W. A., and London, R. I. [1977] “Abstraction and Verification in ALPHARD: Defining and Specifying Iteration and Generators,” CACM 20, 8 (1977) 553–564.
Zilles, S. N. [1974] “Algebraic Specification of Data Types,” Project MAC Progress Report II, MIT (1974), 28–52.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1981 Plenum Press, New York
About this chapter
Cite this chapter
van Emden, M.H., Maibaum, T.S.E. (1981). Equations Compared with Clauses for Specification of Abstract Data Types. In: Gallaire, H., Minker, J., Nicolas, J.M. (eds) Advances in Data Base Theory. Springer, Boston, MA. https://doi.org/10.1007/978-1-4615-8297-7_7
Download citation
DOI: https://doi.org/10.1007/978-1-4615-8297-7_7
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4615-8299-1
Online ISBN: 978-1-4615-8297-7
eBook Packages: Springer Book Archive