Request for tutorial: How to test complicated stateful systems

[saurabhnanda]

Discussion at Reddit: https://www.reddit.com/r/haskell/comments/5jatdg/how_to_use_quickcheck_for_stateful_testing/

I've been looking for examples of how to use Quick Check for "regular" stateful testing, where one would essentially do the following - generate a known input case, call a series of domain APIs, and finally assert the expected system state.

For example, how would one use Quick Check for testing a CRUD JSON API? Or, say a reservation system's domain API, which allows overbooking only if the admin is making the overbooking request?

Even after reading John Hughes' paper on using Quickcheck to test a circular buffer and testing at Volvo & Karla and viewing the accompanying talk I have the following confusion:

• John Hughes' paper has a comment that QuickCheck needs two separate descriptions of the expected behaviour; bugs will be identified in areas where these descriptions don't agree with each other. And the circular queue example also talk about a state model inside the test itself. Does this mean we have to build two systems - the actual one and the one in the test (the simplified model)?
• Do you know if complete QuickCheck tests for the circular buffer example have have shared somewhere? I'd like to go through them to understand how it's possible to build a simplified "state model" without actually rewriting a circular buffer in the test itself.
• How does one pass around the test state (model state) in Haskell's Quickcheck? It's not obvious from the Hackage docs.

[saurabhnanda]

Is the Haskell QuickCheck library (this library) at feature parity with Quviq's QuickCheck? The free version or the paid version? The free version does not have state machine based testing. Is this the reason why I'm unable to sync John Hughes' talk with the Haskell QuickCheck library - http://www.quviq.com/downloads/

[nick8325]

Yes, unfortunately the state machine-based testing is not implemented in Haskell QuickCheck. It would be really nice to have it but no-one has implemented it. Quviq QuickCheck does have more features than Haskell QuickCheck, because of having full-time developers - Haskell QuickCheck is about equivalent to the free version, I would say.

The only special support for testing imperative code in Haskell QuickCheck is the Test.QuickCheck.Monadic module, based on the paper Testing monadic code with QuickCheck. This is a bit more work as you have to think of properties, while with the state machine approach you get the property "for free" after writing the model.

Since you ask, the model in the state machine testing is usually much simpler than the real system because it's implemented in the simplest possible way. For example, for the circular buffer, the model would simply be a list. For dets, I think it was just a list of key-value pairs.

[nick8325]

Having said that, your comment did inspire me to start hacking together a similar library for Haskell QuickCheck. So far, it seems quite plausible (I was worried that the types would get in the way, but they don't really), so maybe this is something we could have in the future.

[saurabhnanda]

Having said that, your comment did inspire me to start hacking together a similar library for Haskell QuickCheck. So far, it seems quite plausible (I was worried that the types would get in the way, but they don't really), so maybe this is something we could have in the future.

Happy to help. Sort of :)

For example, for the circular buffer, the model would simply be a list

How can a simple list be used as a circular buffer without explicitly dealing with the wraparound logic, at which point it become an independent implementation itself?

[saurabhnanda]

This issue is also to seek guidance on how to use QC for real-life stateful apps. It seems the documentation is non-existent around this topic. For example, I can't visualise how to write tests for soemthing like a hotel reservation system.

[saurabhnanda]

If we take the non state-machine approach, what would some properties look like in the case of a hotel reservation system?

• Configure hotel with random number of rooms; apply random set of reservation, cancellation, and modification operations; check that hotel is not oversold on any date? How to bias the operations so that the dates are clustered together? How to bias towards month and year boundaries to uncover date related bugs?
• Configure hotel with random number of rooms; apply set of domain operations; ensure each valid operation is accepted. How to check for validity without reimplementing the validation logic?

[nick8325]

How can a simple list be used as a circular buffer without explicitly dealing with the wraparound logic, at which point it become an independent implementation itself?

In this case the circular buffer was used as a bounded queue, so you're not allowed to overfill it. That means the client can never observe the wraparound, it's purely an implementation detail.

The precondition, postcondition and next-state function for each operation would then look something like this, where the state is given as a list xs:

get:

• precondition: xs /= [].
• postcondition: result = head xs
• next state: tail xs

put(x)

• precondition: length xs < n, where n is the max queue length
• postcondition: none
• next state: xs ++ [x]

[nick8325]

Configure hotel with random number of rooms; apply random set of reservation, cancellation, and modification operations; check that hotel is not oversold on any date?

Sounds reasonable.

How to bias the operations so that the dates are clustered together? How to bias towards month and year boundaries to uncover date related bugs?

This is something you would fix in your Arbitrary instances. For example, you could generate a random month, then choose the date by starting from the first of the month and adding a random offset in days between -30 and 30. By picking the offset in a biased fashion you can generate dates near the first of the month:

genOffset :: Gen Int
genOffset =
  frequency
    [(3, choose (-3, 3)),
     (1, choose (-30, 30))]

Configure hotel with random number of rooms; apply set of domain operations; ensure each valid operation is accepted. How to check for validity without reimplementing the validation logic?

This is a risk of course. You try to avoid it by making the model as simple as possible - no optimisations, no shortcuts. For example, in the hotel you might just define one function which takes the state of the booking system and checks if it's valid (e.g. no overbooking). Then you might say, if the hotel state is valid after making the booking then the booking should be accepted. I don't know the details of the booking system of course, but the point is you can often write the specification in a way which is more declarative than the implementation.

[nick8325]

I agree that we need more documentation around this.

[saurabhnanda]

Do you know of anyone using QuickCheck for common business/domain oriented webapps (as opposed to complicated libraries like streams or parsers or compilers)? Probably motivating them to give a detailed talk or sharing some code can be a good start.

[changlinli]

@saurabhnanda My experience at work is with Scala with ScalaCheck, Scala's equivalent of QuickCheck, (which does have a version of state machine testing that I've basically never used). Unfortunately none of that is shareable and I don't have a great example to show from my own projects, although I'll see if I can whip one up in the coming days.

I do, however, have a bit of experience with how ScalaCheck get used in run-of-the-mill business webapps, which sounds like it might be useful to you. In general, my takeaway has been even if checking the conceptual heart of your application can seem difficult, there's usually enough other incidental properties that are crucial to the correctness of your program to check that QuickCheck (or the equivalent) is something I include in all my work projects these days. Here's a couple of use cases that almost always come up that are usually independent of state checking and can be applied to the pure parts of your code (which are hopefully the majority).

• As a fuzzer. Almost all systems have the property, which is usually fairly easy to test for, "No matter what kind of input, don't crash unexpectedly." QuickCheck is great for this, especially if you've separated your main processing pipeline from the state of your app and can write generators at either end of the pipeline (i.e. feed in arbitrary JSON and feed in arbitrary values from a database). Hell sometimes in my QuickCheck tests, I just make sure my system doesn't crash out with an exception and utterly discard any result. In particular in two domains that come up all the time in business apps QuickCheck is amazing.
  • String processing: Think of all the webpages that break on non-English names... What will my program do if one of my users in my database has accents in their name? Will my fancy product search bar be able to find products with non-English names? Don't worry! QuickCheck will throw strings thought up by Cthulhu himself at yo, I don't even care what my system returnsur program and see if anything topples over.
  • Floating point calculations: Do any of your calculations result in NaNs? Infinities? You probably don't want that... Do you really want your end-user to see a "NaN" show up on the webpage?
• As a correctness check for optimization efforts. I write a first version of some processing pipeline or function, ship it out. Under load it turns out it's not fast enough. I move this original version over to my test code and in my non-test source code start optimizing the hell out of the original. QuickCheck ensures to a high degree of confidence that my optimization efforts have not changed behavior at all.

One small note:

How to check for validity without reimplementing the validation logic?

In addition to what @nick8325 says, I want to add it is often the case that certain invalid states are very easy to describe and check for with QuickCheck and it is often very worthwhile to even get that sort of partial coverage when devising all the necessary generators and structuring your code appropriately for checking full validity is more difficult and time-consuming. That is if you can't check your code always leaves things in a valid state, you can at least check that your code never leaves things in certain obvious invalid states.

In general when I've tested the state of a CRUD system, I've almost always mocked out the persistence layer with something like a Data.Map and then there's usually a baseline of general properties that are worthwhile to always check such as the following:

• What does creating an already existing entity do?
• What does reading/updating/deleting a non-existent entity do?

Your hotel overbooking scenario fits in nicely; if I swapped out my persistence backend for a simple [] of hotel room reservations and then just spewed requests at the system, are there any two entries in my list that have the same room and date?

[bartavelle]

As an illustration of what @changlinli said, here is code that does property testing against complex logic. It runs several games of 7startups, with players playing random cards, and checks that all games terminate without throwing.

The game logic is a free monad, allowing for several interpreters, including a pure one that is used for tests.

Even though this tests a complicated piece of logic by only checking it doesn't crash, a few bugs were found!

[saurabhnanda]

@changlinli thank you for your thoughtful reply 👍

String processing: Think of all the webpages that break on non-English names... What will my program do if one of my users in my database has accents in their name? Will my fancy product search bar be able to find products with non-English names? Don't worry! QuickCheck will throw strings thought up by Cthulhu himself at yo, I don't even care what my system returnsur program and see if anything topples over.

This seems interesting. Do you generate the raw JSON strings and send them over to the WAI endpoint, so that the JSON parsing is also tested, or do you generate the Haskell values that the JSON is supposed to be parsed to. That is, what do you generate: {"name": "random string", "email": "random string"} OR User{userName="random string", userEmail="random string"}

if I swapped out my persistence backend for a simple [] of hotel room reservations

How easy is it to do this in a large-scale webapp? Does this basically mean all database accesses need to go via some sort of app-specific DB library (which is written on top of the underlying DB library, i.e. Persistent, Opaleye, or PG-Simple), which can then be swapped out with an in-memory implementation during testing? Isn't this too much work?

[stevana]

I played around a bit and managed to get something that looks similar to Erlang quickcheck's state machine approach: https://gist.github.com/stevana/1595f3190c87220c59caaaf7c2aae04b .

It seems to me that the generator, shrink function, and the safety property are quite generic (they only use the pre-conditions, the model transition functions and the post-conditions). So I'd like to see how much of that code we can template Haskell away.

I also wonder if one can do away with the trace? I couldn't figure out how to show and shrink things like pop without it. Also if one wants to test for race conditions one will need something similar to the trace anyhow?