Broad Stateful Testing

Getting started

We’ll start with a very wide scan of the system to make sure the basic stuff works. This will check for simple API misunderstandings, errors that type analysis couldn’t reveal, or issues with configuration or the basic test setup.

The property

Let’s start off by adding the actual property declaration to our module. Take a look at the property in the code provided below in the test/bookstore_test.exs file.

In the property, we’ll make use of the ?SETUP macro to boot the bookstore OTP application once for all the tests, ensuring that all libraries and dependencies are in place. We’ll then call the Bookstore.DB.setup/0 and Bookstore.DB.teardown/0 functions on each iteration to get rid of the database table and its state between each test so that the execution is clean.

We can now start on the model.

The model

For the model, we’ll do nothing but function calls to keep employing the skills we learned during broad testing.

The model is defined in the code provided below from line 41 to line 58

The command/1 function is the only significant function. For now, the other functions do not affect the testing. The precondition and postcondition states are always true. As for the next_state, it has no effect on the working of the application.