Sufficient completeness is the property that every operation in a specification is defined on all valid inputs. It is important property both for developers of specifications, to check that they have not missed a case in defining operations, and to inductive theorem provers, to check the soundness of a proposed induction scheme. The Maude Sufficient Completeness Checker is an experimental tool designed to check this property for confluent and terminating Maude specifications. The tool currently comes in two different versions, each with different features:
The primary author is Joe Hendrix who can be contacted for questions about the tool.
The narrowing-based version of the tool has been integrated into the Maude Inductive Theorem Prover (ITP), and is available for download from the ITP's homepage. These downloads include a README for using the tool and a few examples. For details on the theory behind the tool, take a look at the papers below.
The tree automata-based version requires an extended version of Maude 2.3. We offer pre-built binaries for GNU/Linux and x86 processors along with a source distribution. The source distribution requires the Ceta tree automata library be installed along with the usual requirements for compiling Maude.
scc.maude is in the current directory, you must load it using
the command:
Maude> load scc.maude
You then enter in modules that you are interested in checking using the
usual syntax. When you are ready to check sufficient completeness, you then
type the following commands.
Maude> select SCC-LOOP .
Maude> loop init-scc .
Maude> (scc ModuleName .)
As an example, we provide the following transcript of using the sufficient
completeness checker on the predefined module QID-LIST in
prelude.maude:
\||||||||||||||||||/
--- Welcome to Maude ---
/||||||||||||||||||\
Maude-ceta 2.3 built: Feb 18 2007 9:49:47
Copyright 1997-2007 SRI International
With CETA extensions Copyright 2006-2007
University of Illinois at Urbana Champaign
Sun Feb 18 10:44:31 2007
Maude> load scc
Maude> select CC-LOOP .
Maude> loop init-cc .
Starting the Maude Sufficient and Canonical Completeness Checker.
Maude> (scc QID-LIST .)
Checking sufficient completeness of QID-LIST ...
Success: QID-LIST is sufficiently complete under the assumption that it is
weakly-normalizing, ground confluent, and ground sort-decreasing.
Maude>
The narrowing-based tool is described in our RTA tool paper. We also have an extended technical report with more detailed proofs.
The theoretical work related to the tree automata-based approach is discussed in the following two technical reports. The first discusses sufficient completeness in a very general context, and then shows how the order-sorted linear subset of that class can be checked using a class of tree automata called Propositional Tree Automata which are closed under an equational theory and boolean operations, The second explores Propositional Tree Automata in more detail, and shows how we check emptiness for associative and associative and commutative theories.