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 the
Registry
and RegistryModel
module from the test suite, which respectively implement and model 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.