Specification and Proof in Membership Equational Logic
This paper is part of a long-term effort to increase
expressiveness of algebraic specification languages while at the same
time having a simple semantic foundation on which efficient execution by
rewriting and powerful theorem-proving tools can be based. In
particular, our rewriting techniques provide semantic foundations for
Maude's functional sublanguage, where they have been efficiently
implemented.
This effort started in the late seventies, led by the ADJ group,
who promoted equational logic and universal algebra as the semantic
basis of program specification languages. An important later milestone
was the work around order-sorted algebras and the OBJ family of
languages developed at SRI-International in the eighties. This effort
has been substantially advanced in the mid-nineties with the
development of Maude, a language based on membership equational logic.
Membership equational logic is quite simple, and yet quite powerful.
Its atomic formulae are equations and sort membership assertions, and
its sentences are Horn clauses. It extends in a conservative way both
(a version of) order-sorted equational logic and partial algebra
approaches, while Horn logic with equality can be very easily encoded.
After introducing the basic concepts of the logic, we give conditions
and proof rules with which efficient equational deduction by rewriting
can be achieved. We also give completion techniques to transform a
specification into one meeting these conditions. We address the
important issue of proving that a specification protects a
subspecification, a property generalizing the usual notion of
sufficient completeness. Using tree-automata techniques, we develop a
test-set based approach for proving inductive theorems about a
parameterized specification.
We briefly discuss a number of extensions of our techniques, including
rewriting modulo axioms such as associativity and commutativity, having extra
variables in conditions, and solving goals by narrowing.
Finally, we discuss the generality of our approach and how it extends
several previous approaches.
full paper