Skip to content


Subversion checkout URL

You can clone with
Download ZIP
Haskell Contracts Checker
Haskell Shell

Committing a light version of the testsuite that does

not contain any CF contracts, in order to experiment
completeness and finite models without the CF-related
complications. The examples are taken from new-testsuite/

There is already an interesting finding: the append contracts
hold (and 'minrec' is able to say UNSAT), but they appear to
be non-provable (SAT) in master branch. I don't really know
what to say, but there must be something incomplete in master.

NB: 'minrec' vs 'min' does not play a role here -- minrec only
has to do with CF and there are no CF contracts in this testsuite.
latest commit af501bd083
@dimitriv dimitriv authored

Haskell Contracts Checker

Installation instructions

First, you need to pull halo, the Haskell to Logic Translator:

git submodule update --init

Then, in the main directory, run

cabal install

This installs the hcc executable.

Running the testsuite

The testsuite is in the testsuite directory, with an own readme.

Something went wrong with that request. Please try again.