PLT-3313: Property based tests for theorems in Isabelle

input-output-hk / marlowe

Prototype implementation of domain-specific language for the design of smart-contracts over cryptocurrencies

Apache License 2.0

172 stars 43 forks source link

PLT-3313: Property based tests for theorems in Isabelle #167

Closed yveshauser closed 1 year ago

yveshauser commented 1 year ago

This PR adds FixInterval and ReduceContractUntilQuiescent to the test-spec protocol together with property based tests for theorems stated in Isabelle. A prerequisite for that is the SemiArbitrary type class (similar to the one in marlowe-cardano), which is also introduced here.