Wrapping Up

Summary

This chapter has shown us the basics of stateful property testing, based on a single simple model. We’ve been through the two phases of the testing:

1. Symbolic testing, where the model is used to generate a sequence of commands that represents what the system should do.
2. Real testing, where the symbolic sequence of commands is applied to the real system, and the results compared with what the model expects.

We’ve put these concepts in practice through a cache server modeled as a first-in-first-out list and showed that the model seems to hold fine under sequential operations. We’ve then seen how PropEr can take that same exact model and create a parallel version of it that could, with some amount of help, find concurrency bugs in our cache program.

What’s next

We’ve seen the base mechanism of how stateful properties work, but truth be told, the cache example we used resulted in a rather simple model. In the next chapter, we’ll experiment with a more complex stateful system based on SQL queries, with varying amounts of determinism. We’ll move past the basics of stateful properties and explore more advanced techniques to handle the complexity of modeling large systems for integration tests.