README.md

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

Building

Without nix

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
  

With nix

This repository comes with some nix files which might or might not help hacking on quickcheck-dynamic simpler. Before you start using nix, please make sure you've configured haskell.nix caching as per those instructions.

• Building with nix should be as simple as:

  nix-build -A quickcheck-dynamic.components.library
  

• To enter a shell providing basic development tool:

  nix-shell
  

  This can automated using direnv:

  direnv allow
  

• Then go back to Without nix instructions