quickcheck-dynamic

A library for testing stateful programs using QuickCheck and dynamic logic.

This repository hosts:

The core quickcheck-dynamic library providing tools for quickchecking stateful models,
Example of integrating io-sim's Haskell runtime simulator and quickcheck-dynamic to model and test complex multi-threaded application.

Documentation

The original stateful testing approach is described in John Hughes' research paper: https://www.cs.tufts.edu/~nr/cs257/archive/john-hughes/quviq-testing.pdf
The Registry example is a common case study that's been explored in two papers:
- How well are your requirements tested?
- and Understanding Formal Specifications through Good Examples
The dynamic logic addition allows you to specify that after a generated test sequence, the system is able to reach a specific required state. In other words, you can specify that some "good" state is reachable from any possible state.

The following talks provide concrete examples on how this approach is used to test smart contracts in Plutus:

John Hughes high level talk on how to test Plutus smart contracts using this library: https://youtu.be/V9_14jjJiuQ
55 minutes in to this lecture an example of using the state machine formalism: https://www.youtube.com/watch?v=zW3D2iM5uVg&t=3300

The following blog posts and talks provide some more in-depth educational material on quickcheck-dynamic:

Edsko de Vries wrote a nice post to compare quickcheck-dynamic with quickcheck-state-machine, another library to write model-based tests on top of QuickCheck. This blog post introduces quickcheck-lockstep which provides lockstep-style testing on top of quickcheck-dynamic,
IOG published an introductory post on quickcheck-dynamic, detailing some rationale and background for this work, and suggesting a step-by-step approach to use it based on some real world experience.
A presentation from BOBKonf 2024 which provides a good overview of why one would want to use such a library, how it's been applied in some concrete projects, and some basic understanding of the mechanics.

This package uses Cabal-based build. To build from source:

Ensure both ghc and cabal executables are in your PATH.
- ghcup is a great way to manage Haskell toolchain.
- quickcheck-dynamic currently requires a GHC version > 8.10
Run
```
cabal update && cabal build all
```
To run tests:
```
cabal test all
```

This repository uses nix to provide a development and build environment.

For instructions on how to install and configure nix (including how to enable access to our binary caches), refer to this document.

If you already have nix installed and configured, you may enter the development shell by running nix develop.