Combining Algebraic and Set-Theoretic Specifications (Extended Version)

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


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.

Full Text:


This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.

ISSN: 0909-0878 

Hosted by the Royal Danish Library and Aarhus University Library