The Maude Sufficient Completeness Checker


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.

Narrowing-based Sufficient Completeness Checker

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.

Tree Automata-based Sufficient Completeness Checker

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.


Usage of the tree automata-based checker. You must first make sure the sufficient completeness checker is loaded, assuming the checker source 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.


The narrowing-based tool is described in our RTA tool paper. We also have an extended technical report with more detailed proofs.

A Sufficient Completeness Reasoning Tool for Partial Specifications
Joe Hendrix, Manuel Clavel, and José Meseguer
In Proc. Rewriting Techniques and Applications, 2005, Springer-Verlag LNCS 3467, 165–174, April 2005.
RTA Paper (PDF)©Springer-Verlag, Extended technical report (PDF)

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.

Sufficient Completeness Checking with Propositional Tree Automata
Joe Hendrix, Hitoshi Ohsaki, and José Meseguer
Report No. UIUCDCS-R-2005-2635 (Engr. No. UILU-ENG-2005-1825), September 2005
Technical report (PDF)

Propositional Tree Automata
Joe Hendrix, Hitoshi Ohsaki, and Mahesh Viswanathan
Report No. UIUCDCS-R-2006-2695 (Engr. No. UILU-ENG-2006-1726), February 2006
Technical report (PDF)