# Coneqct: a contextual equivalence checking tool for Interface Middleweight Java

## 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