Clone wiki

coneqct / Home

Coneqct: a contextual equivalence checking tool for Interface Middleweight Java

Home | Downloads | Syntax | Examples

Requirements

The checker runs on the .NET platform (>=4.5), and hence requires a recent implementation of the .NET Common Language Infrastructure (CLI) to be installed on your system.

Installation

  1. Download the latest assemblies from downloads. All the required assemblies are packaged together in a zip file named "coneqct-XXX.zip" where "XXX" denotes the revision number.

  2. Unzip to any convenient location, this creates a new directory "coneqct-XXX" in which resides the executable "coneqct.exe".

  3. To verify that all is well, on the command line navigate to the directory "coneqct-XXX" and run the command:

    • ".\coneqct.exe" on Windows or,
    • "mono ./coneqct.exe" on Linux or Mac. If the installation is working correctly, the usage message will be printed out to the terminal.

Usage

On Windows, to check the equivalence of two IMJ terms defined in the file "terms.inp", run:

> .\coneqct.exe \path\to\terms.inp

On Linux or Mac you should prefix this command by "mono" (and use appropriate slashes):

> mono ./coneqct.exe /path/to/terms.inp

A number of example inputs are bundled with the installation. For example, after navigating to the root of the directory "coneqct-XXX", to verify the "extended types" equivalence adapted from Benton and Leperchey's "Relational Reasoning in a Nominal Semantics for Storage" on Mac, run:

> mono ./coneqct.exe inputs/inp2.imj

See Syntax for a detailed description of the syntax of the input file format.

The tool can be configured using some command-line options:

  • -maxint <int>: set the value of maxint to <int>.
  • -pc1, -pc2: write out the canonical form of the first, respectively second, term to the terminal.
  • -pa1, -pa2: write out a dot-format representation of the first, respectively second IMJ automaton to files "auto1.dot", respectively "auto2.dot".

For example, to check the equivalence defined in "inputs/inp3.imj" with the largest integer set to 5 on Linux, enter the command:

> mono ./coneqct.exe -maxint 5 ./inputs/inp3.imj

Typically, interesting equivalences do not depend on the particular value of maxint, so it is best to keep maxint small in order to increase efficiency of verification.

Updated