Circ
From FSL
Circ is an automated prover that is implemented as an extension of Maude. Circ implements the circularity principle, which generalizes both circular coinduction and structural induction, and can be expressed in plain English as follows. Assume that each equation of interest (to be proved) e admits a frozen form fr(e) and a set of derived equations, its derivatives, Der(e). The circularity principle requires that the following rule be valid: if from the hypotheses H together with fr(e) we can deduce Der(e), then e is a consequence of H. When fr(e) freezes the equation at the top, the circularity principle becomes circular coinduction. When the equation is frozen at the bottom on a variable, then it becomes a structural induction (on that variable) derivation rule. This way, Circ supports both coinduction and induction as projections of a more general principle.
Web Interface to Circ
There are two methods available for running Circ. First, the Circ prover can be downloaded (see below) and run directly. This requires Maude, linked below, to be installed. Second, Circ can be executed using an online interface (click the "Try it online" icon above), which provides a place to enter and run existing or new proof scripts.
Documentation
Installation
- If you already have Maude installed, then go to the next step. Otherwise,
- if you work on a Linux platform, then go to Maude download page and follow the steps written there for downloading and installing Maude;
- if you work on a Windows platform, then download Maude for Windows;
- if you have Eclipse, then you also may download Maude Development Tools; this include a set of plug-ins embedding the Maude system into the Eclipse environment.
Download CIRC 1.4: 
Circ.zip 
. The archive includes documentation, a set of examples, and the tool circ.maude.
- Copy the file circ.maude in the folder including Maude tools (e.g., full-maude.maude, model-checker.maude and so on).
Loading
- Start Maude in Full-Maude mode. If Full-Maude is not loaded automatically, then introduce the command
in full-maude
- Load the prover introducing the command
in circ
- You may introduce now any CIRC or Full-Maude command.
Running the Examples
The system is accompanied by a set of examples exhibiting the power of the prover. The usual scenario for running an example is:
- set the prover in the initial state introducing Maude command
loop init .
- In many cases this is an optional step.
- introduce Maude specifications using Maude command
in file-name
- The files include specifications and commands. The complete list of CIRC commands is included in the
CIRC User Manual .
Information about Circ is also available at the Circ mirror site in Romania.
