The Maude Termination Assistant

Abstract

We present the Maude Termination Assistant (MTA). Its purpose is to complement the fully automatic Maude Termination Tool (MTT) [2] in two ways: (i) to help users find a proof when MTT may not find one; and (ii) for teaching purposes. The main features supported by MTA are: (1) termination proofs of order-sorted equational theories, which may include conditional rules without extra variables; (2) such proofs can be modulo any combination of associativity and/or commutativity and/or identity axioms; (3) identity axioms are automatically transformed into rules by a semantics-preserving theory transformation; (4) support for user-specified recursive path orders modulo any combination of the above axioms; and (5) support for user-specified linear polynomial orders modulo any combination of the above axioms.

Downloads

We have provided a tar archive of our code with example files. The examples will run with version 2.7.1 of Maude (and probably newer versions as well). Binaries and source are downloadable from the Maude website.

Instructions

1. Take a Maude module in some file (say the module FOO in file foo.maude ) that you wish to analyze and annotate each operator in FOO with a metadata attribute that defines how the operators are to be ordered.
2. Load the Maude file you just annontated into the Maude interpreter by typing

    $ maude ~/ex/foo.maude 

   at the command prompt, assuming your example is in a folder ex which is a subdirectory of your home folder and that the Maude binary is located on your PATH.
3. Initialize the MTA tool by typing

    Maude> load ~/mta/mta.maude 

   at the Maude prompt, assuming you unzipped the tool tarball inside your home folder.
4. Check module termination using the AvC-RPO or polynomial orderings using the commands:

   1.  (check-poly FOO .) 

      or;

   2.  (check-AvCrpo FOO .) 

$ maude ~/mta/test/acrpo/example_name.maude

$ maude ~/mta/test/poly/example_name.maude