The ITP tool

Summary

The ITP tool is a theorem prover that can be used to prove properties of membership equational specifications, as well as incompletely specified algorithms on them, as a way to support incremental development of specifications.

Membership equational logic is an expressive version of equational logic, particularly adequate for specifying and verifying semantic data structures, such as ordered lists, binary search trees, priority queues, and powerlists.

Sources

The ITP tool is a Maude program that makes extensive use of the reflective capabilities of this system. In fact, rewriting-based proof simplification steps are directly executed by the powerful underlying Maude rewriting engine.

The ITP tool is currently available as a web-based application that includes a module editor, a formula editor, and a command editor. These editors allow users to create and modify their specifications, to formalize properties about them, and to guide their proofs by filling and submitting web forms. The web application also offers a goal viewer, a script viewer, and a log viewer. They generate web pages that allow the user to check, print, and save the current state of a proof, the commands that have guided it, and the logs generated in the process by the Maude system.

The ITP Web tool can be executed in two different ways: either as a remote or as a local application. The only requirements to run the remote application are a computer with an Internet connection and JDK 1.4.1 installed (it should be available on most computers), and a browser. The remote application can be accessed at the URL

http://maude.sip.ucm.es:8080/webitp/

Running the ITP tool as a local application is more demanding. In addition to JDK 1.4.1 and a browser, it is also necessary to have the Tomcat server installed, as well as Maude and the files containing the specification of the ITP.

Documentation

The ITP tutorial contains the most up to date documentation. It also presents membership equational logic and discusses its adequacy for the specification and verification of semantic data structures, such as ordered lists, binary search trees, and powerlists. The SCC tool has been written in Maude and relies on Maude's reflective capabilities and the ITP tool. The SCC tool is included in the latest distribution of the ITP tool, and it can be executed both in stand-alone mode and through appropriate commands during an ITP session. --->

Manuel Clavel
9 May 2006