Introducing Model_quickcheck. Quickcheck for stateful, imperative code

Hi there!

I’m sharing a small project I’ve been working on that I hope will be interesting or useful to the community. Model_quickcheck is a model-based testing system that allows you to validate the “properties” of stateful, imperative OCaml programs. It’s built on Jane Street’s Base_quickcheck. I’d love to read your thoughts.

I just started learning OCaml and one of the first projects I’ve been working on is a user-space reliable transport protocol. Writing tests for this system became unwieldy because I was trying to validate certain properties of the protocol by thinking up very specific sequences of actions that would invoke behaviors that relied on that property. I got tired of it and got curious if there was a way to generate these interesting sequences. My research turned up frameworks like QCSTM[0] and PropEr[1] for state machine property-based testing. This seemed to be exactly what I needed so I started building something similar.

To use Model_quickcheck you specify a set of actions to apply to your program, a model that describes the state of you program and a set of predicates that define the properties of you system. The model is hopefully a simpler representation of your system e.g. a map instead of a key-value database, or a queue instead of a reliable network protocol. Model_quickcheck then generates a random sequences of actions applies them to your system and verifies the properties.

This has been an exciting and useful project. I’ve learned a bunch about the Base library, Quickcheck, first class modules, and inline tests. I’m just getting started, but I just wanted to share the project with the community since I’ve learned a lot by lurking here.

[0] ~https://github.com/jmid/qcstm~
[1] ~https://propertesting.com/book_state_machine_properties.html~

4 Likes