- and

-Logics

Claus Hintermeier
Hélène Kirchner
Peter D. Mosses

December 1996

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

Available as PostScript, PDF.

Last modified: 2003-06-08 by webmaster.