quickcheck-dynamic
A library for stateful property-based testing
https://github.com/input-output-hk/quickcheck-dynamic#readme
| LTS Haskell 24.28: | 4.0.1 |
| Stackage Nightly 2026-01-18: | 4.0.1 |
| Latest on Hackage: | 4.0.1 |
quickcheck-dynamic-4.0.1@sha256:00940c7b9a391bd2786c9239985f13f91ef990ae803cc54790ddb7484a0f0505,2640Module documentation for 4.0.1
- Test
- Test.QuickCheck
- Test.QuickCheck.DynamicLogic
- Test.QuickCheck.DynamicLogic.CanGenerate
- Test.QuickCheck.DynamicLogic.Internal
- Test.QuickCheck.DynamicLogic.Quantify
- Test.QuickCheck.DynamicLogic.SmartShrinking
- Test.QuickCheck.DynamicLogic.Utils
- Test.QuickCheck.Extras
- Test.QuickCheck.StateModel
- Test.QuickCheck.StateModel.Variables
- Test.QuickCheck.DynamicLogic
- Test.QuickCheck
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
RegistryandRegistryModelmodule 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.
Changes
Changelog
All notable changes to this project will be documented in this file.
The format is based on Keep a Changelog, and this project adheres to Semantic Versioning.
As a minor extension, we also keep a semantic version for the UNRELEASED
changes.
4.0.1 - 2025-07-14
- Added support for
Quickcheck-2.16.
4.0.0 - 2025-03-12
- BREAKING: Removed
Realized- To migrate uses of
RealizedwithIOSim, index the state type on the choice ofRunModelmonad and index the relevant types:-- Turn: data ModelState = State { threadId :: Var ThreadId } -- Into: data ModelState m = State { threadId :: Var (ThreadId m) }
- To migrate uses of
- BREAKING: Moved
Error statefromStateModeltoRunModeland indexed it on both thestateand the monadm - BREAKING: Changed
PerformResultfromPerformResult (Error state) atoPerformResult state m a - Added a
moreActionsproperty modifier to allow controlling the length of action sequences.
3.4.1 - 2024-03-22
- #70 Expose
IsPerformResulttypeclass
3.4.0 - 2024-03-01
- Added some lightweight negative-shrinking based on a simple dependency analysis.
- Added the option to return errors from actions by defining
type Error state. When this is definedperformhas return typem (Either (Error state) (Realized m a)), when it is left as the default the type remainsm (Realized m a). - Changed
withGenQto require a predicate when defining aQuantification. Note: This is technically a breaking change as the interface changed
3.3.1
- Adapt code to not constrain mtl version too much
3.3.0
- Added suppport for GHC 9.6.2 compiler
3.2.0
- Added support for negative testing via
validFailingActionandpostconditionOnFailurecallbacks inStateModelandRunModel.
3.1.1 - 2023-06-26
- Added instances for
HasVariableswith custom error messages to avoid the issue of missingGenericinstances causing difficult to understand type errors.
3.1.0 - 2023-04-10
- BREAKING: Change the type of
postconditionto allow you to express property monitoring (e.g. stats or counterexamples) in the postcondition itself - rather than duplicating code for counterexamples in themonitoringfunction.
3.0.3 - 2023-04-18
- Added
hasNoVariablesQandforAllNonVariableDLfunctions to help make quantification require less boilerplate inDLproperties.
3.0.2 - 2023-02-17
- Added instances of
HasVariablesfor Word types - Exported definition of
HasNoVariablesto make it useable with deriving via in downstream packages (whoops!) - Fixed impossible to use
nextVararguments toforAllUniqueDL
3.0.1 - 2023-02-15
- Remove template haskell dependency
3.0.0 - 2023-02-14
- BREAKING: Add
HasVariablesclass to keep track of symbolic variables and automatically insert precondition checks for well-scopedness of variables. - BREAKING: Remove some unnecessary and unusead features in dynamic logic, including re-running tests from a counterexample directly.
- Improved printing of counterexamples in DL - they are now printed as code that can be copied more-or-less verbatim to create a runnable counterexample in code.
- Made the variable context explicit to avoid having to keep track of symbolic variables in the model
- This introduces the
ctxAtTypeandarbitraryVarfunctions to use in action generators (c.f. theRegistryModel.hsexample).
- This introduces the
2.0.0 - 2022-10-11
- BREAKING: Add
Realizedtype family to distinguish between the model- and real type of an action - BREAKING: Introduce
RunModeltype class to interpret Model-generated sequence of actions against real-world implementation- Move
performmethod fromStateModelto this new type-class - Also split
postconditionandmonitoringout from theStateModelto theRunModeltype class
- Move
- Added Thread registry example based on io-sim concurrency simulation library
1.1.0 - 2022-08-27
- Fix broken links in Hackage-generated documentation and link to other Quviq papers
- Add
Show aconstraint onmonitoring
1.0.0
- Initial publication of quickcheck-dynamic library on Hackage
- Provide base
StateModelandDynamicLogictools to write quickcheck-based models, express properties, and test them