This paper is part of an effort to increase the expressiveness of algebraic specification languages while at the same time having a simple semantic basis on which both the operational semantics of such languages, and theorem proving tools supporting formal verification can be based. In particular, the semantic concepts and proof techniques that we propose have emerged out of, and provide foundation for, work on the functional sublanguage of Maude, which extends in substantial ways the OBJ language.
Regarding expressiveness of algebraic specifications, it has for a long time been recognized that it is very important in practice to support subsorts, partiality, errors, and overloading of function symbols. Our ideas extend and unify within a simple semantic framework two different lines of work in algebraic specification, namely the order-sorted approach initiated by Goguen in the late 1970's, and different partial algebra approaches. The theoretical framework on which this unification is achieved is quite simple. We assume a family K of kinds, and a many K-kinded signature of operations. Each kind has an associated set of sorts. Each sort is interpreted as a unary membership predicate, defining a subset at the level of the algebras. Formulae are Horn clauses on equations and membership predicates. The intuitive interpretation is that data elements that have a kind, but do not have a sort are undefined, or error elements. Axioms in a specification can prescribe subsort inclusions, as well as definedness of an overloaded operator for different arity and coarity sorts.
The simplicity of the membership algebra framework allows an efficient operational semantics by rewriting (or narrowing when a specification is seen as a logic program in the PROLOG sense) that makes specifications executable. Such a semantics, which justifies many of the design decisions made in the implementation of Maude, is investigated in detail in this paper, by deriving from the general deduction rules for the logic more efficient equivalent rules for rewriting under reasonable assumptions about the oriented equations. In this regard, the simplicity of our framework provides a satisfactory solution to many problems, like sort-decreasingness, that the more restrictive logics had to face. One of the main problems with the earlier approaches was that sort-decreasingness was not closed under completion. This is no more the case here, since we can easily add semantic-preserving membership axioms. This is a main advantage over previous (some of them quite complex) attempts to settle this question.
Besides operational semantics and completion techniques, we also study in detail theorem proving techniques supporting verification of specifications in membership equational logics. Such techniques include methods for proving sufficient completeness of a specification relative to a subspecification of constructors, and inductive proof techniques that extend the many-sorted test-set based inductive theorem proving approach to the more expressive context of membership specifications. An important ingredient of this extension is the encoding of a relevant subset of membership equational logic specifications as tree automata with equality (and membership) tests. We also consider the extension of these techniques to reason about parameterized specifications. In both cases, the main novel aspect of our technique is to refine a given conjecture step by step until it does not contain any more defined symbols.
(BibTeX entry) (gzip'ed Postscript)