Combining Algebraic and Set-Theoretic Specifications (Extended Version)

Abstract

Specification frameworks such as B and Z provide power sets and cartesian
products as built-in type constructors, and employ a rich notation for
defining (among other things) abstract data types using formulae of predicate
logic and lambda-notation. In contrast, the so-called algebraic specification
frameworks often limit the type structure to sort constants and
first-order functionalities, and restrict formulae to (conditional) equations.
Here, we propose an intermediate framework where algebraic specifications
are enriched with a set-theoretic type structure, but formulae remain in the
logic of equational Horn clauses. This combines an expressive yet modest
specification notation with simple semantics and tractable proof theory.