Contra is a small functional programming language designed to automate the process of finding algebraic counter-examples with property-based testing.

With Contra, you can define properties and check them automatically without the need to write a generator by hand. In particular, can check properties that take user-defined algebraic data types. Even mutually recursive ones!

Contra uses SMT solvers (currently Z3 via the Haskell library SBV) behind the scenes to actually find the counterexamples.

Its main contribution, and the reason you might find using Contra to be easier than using QuickCheck or SBV directly, is that Contra has a completely regular ML-style syntax, which is purposefully similar to Haskell's, and you don't need to learn any special syntax to get started.

This repo includes a file contra/app/MainPretty.hs which is a version of Contra that uses Unicode symbols. This is prettier, but not supported by all terminals. If you do have Unicode support where you plan to run Contra, you can build and install as normal, but use the executable called contra-pretty instead of contra.

You need to have both the SMT solver Z3 and the Haskell build tool Stack installed.

With Z3 and Stack installed, you can clone the repo, using either HTTPS or SSH:

# with HTTPS:
git clone https://github.com/SophieBosio/contra.git

# with SSH:
git clone [email protected]:SophieBosio/contra.git

Navigate to the cloned contra repository.

Build with Stack, optionally using the --pedantic flag:

stack build

Test with Stack, optionally using the --pedantic flag:

stack test

Install with Stack:

stack install

This should install an executable called contra on your system.

If you're not familiar with property-based testing, there are examples in the ./examples folder in this repository. I can also recommend reading John Hughes' paper Experiences With QuickCheck: Testing the Hard Stuff and Staying Sane.

Write a program with some properties, then, with Contra installed, check all the properties with:

contra --check <program-name>.con

Like a normal programming language, you can also execute Contra programs. By default, Contra looks for a function called main and executes it if it exists.

contra <program-name>.con

This prototype also comes with a rudimentary REPL. Start a blank interactive session by typing just contra.

Load files into the REPL with :l <filename>.con and quit with :q.

You can save function definitions (and nullary functions/constants) for the session by using the special syntax def x = ....

# blank REPL session
contra

You can ask Contra to parse and type-check a program and print out the syntax-desugared version of your program.

# parse, type-check and print program
contra --type <program-name>.con

See version info.

contra --version

And ask to see all available options.

contra --help

The design and implementation of Contra were part of my MSc thesis at the University of Oslo, delivered 2024. I was supervised by Michael Kirkedal Thomsen and Joachim Tilsted Kristensen. I'm deeply grateful to them for their help and guidance.

Contra is built based on the pioneering property-based testing tool, QuickCheck.

The underlying machinery in Contra uses the SMT solver Z3.

The particular solver library chosen for this implementation is the Haskell package sbv.