I would like to show how one can apply property based testing to “real-world” programs, such as a CRUD web server application. I’m interested in properties about the system as a whole, not merely some pure parts of it (e.g. serialising and deserisalising to and from JSON).

To achieve this I’ve implemented a Haskell library on top of QuickCheck that makes it possible to specify the correctness of the system using pre- and post-conditions over a state machine model a la Erlang’s proprietary version of QuickCheck.

I’ll explain how the library works and demo how one can use it to specify the correctness of and test a simple CRUD web application. In the process we will expose bugs in the program logic as well as a race condition.

Finally, I’ll compare and contrast the approach presented to other similar tools: Z/B-method/Event-B, TLA+, and Jepsen.