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.
Changes
Changelog
All notable changes to this project will be documented in this file.
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 defined perform has return type m (Either (Error state) (Realized m a)),
when it is left as the default the type remains m (Realized m a).
Changed withGenQ to require a predicate when defining a Quantification. Note: This is technically a breaking change as the interface changed
Added support for negative testing via validFailingAction and postconditionOnFailure
callbacks in StateModel and RunModel.
3.1.1 - 2023-06-26
Added instances for HasVariables with custom error messages to avoid the issue of
missing Generic instances causing difficult to understand type errors.
3.1.0 - 2023-04-10
BREAKING: Change the type of postcondition to allow you to
express property monitoring (e.g. stats or counterexamples) in the
postcondition itself - rather than duplicating code for counterexamples
in the monitoring function.
3.0.3 - 2023-04-18
Added hasNoVariablesQ and forAllNonVariableDL functions to help make
quantification require less boilerplate in DL properties.
3.0.2 - 2023-02-17
Added instances of HasVariables for Word types
Exported definition of HasNoVariables to make it useable
with deriving via in downstream packages (whoops!)
Fixed impossible to use nextVar arguments to forAllUniqueDL
3.0.1 - 2023-02-15
Remove template haskell dependency
3.0.0 - 2023-02-14
BREAKING: Add HasVariables class 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 ctxAtType and arbitraryVar functions to use in action generators (c.f. the
RegistryModel.hs example).
2.0.0 - 2022-10-11
BREAKING: Add Realized type family to distinguish between the model- and real type of an action
BREAKING: Introduce RunModel type class to interpret Model-generated sequence of actions against real-world implementation
Move perform method from StateModel to this new type-class
Also split postcondition and monitoring out from the StateModel to the RunModel type class
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 a constraint on monitoring
1.0.0
Initial publication of quickcheck-dynamic library on Hackage
Provide base StateModel and DynamicLogic tools to write quickcheck-based models, express properties, and test them