Combining Algebraic and Set-Theoretic Specifications (Extended Version)

  • Claus Hintermeier
  • Hélene Kirchner
  • Peter D. Mosses

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.
Published
1996-06-22
How to Cite
Hintermeier, C., Kirchner, H., & Mosses, P. (1996). Combining Algebraic and Set-Theoretic Specifications (Extended Version). BRICS Report Series, 3(52). https://doi.org/10.7146/brics.v3i52.20055