quickcheck-dynamic

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

Background

This library was initially designed by QuviQ in collaboration with IOG to provide a dedicated test framework for Plutus "Smart contracts". As the need of a Model-Based Testing framework arises in quite a lot of contexts, it was deemed useful to extract the most generic part as a standalone package with no strings attached to Plutus or Cardano.

Usage

• Documentation is currenly mostly provided inline as Haddock comments. Checkout StateModel and DynamicLogic modules for some usage instructions.
• For a concrete standalone example, have a look at Registry and RegistryModel modules from the companion quickcheck-io-sim-compat package (not currently available on hackage), a multithreaded Thread registry inspired by the Erlang version of QuickCheck described in this article
• For more documentation on how to quickcheck-dynamic is used to test Plutus DApps, check this tutorial.
• Apart from Plutus, this library is now in use in the Hydra project to verify the Head Protocol implementation with respect to the original research paper.