Equations Compared with Clauses for Specification of Abstract Data Types

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.