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