Coneqct: a contextual equivalence checking tool for Interface Middleweight Java
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.
On Windows we recommend Microsoft's ".NET Framework", the latest stable version is 4.5.2: https://www.microsoft.com/en-us/download/details.aspx?id=42643.
On Linux or Mac we recommend Xamarin's "Mono": http://www.mono-project.com/download/
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.
Unzip to any convenient location, this creates a new directory "coneqct-XXX" in which resides the executable "coneqct.exe".
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.
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.