Precise Stateful Modelling
Take a look at the precise tests using a shim module that will uncover new bugs in the code and the test.
We'll cover the following...
Getting started
It’s time we use a model to dig deeper into what the system can or can’t do. Once again, a critical property of models is that they are simpler but sufficient enough to represent the real thing. For our database, a map will prove sufficient to track all changes. Before we start to add postconditions, we may want to make an inventory of all the kinds of operations we’ll want to check:
- Adding a book that is not yet in the system is expected to succeed.
- Adding a book that is already in the system is expected to fail.
- Adding a copy of a book that is already in the system is expected to succeed and make one more copy available immediately.
- Adding a copy of a book that isn’t yet in the system should return an error.
- Borrowing a book that is in the system and available makes one less copy available.
- Borrowing a book that is in the system but unavailable returns an error saying it is unavailable.
- Borrowing a book that is not in the system would return an error saying it is not found.
- Returning a book that is in the system makes it available again.
- Returning a book that is not in the system returns an error saying it was not found.
- Returning a book that is in the system but for which all copies are accounted for returns an error as well.
- Looking up a book by ISBN should succeed if the book is in the system already.
- Looking up a book by ISBN should fail if the book is not in the system yet.
- Searching for a book by author should succeed if the submitted name matches a part of or the full name of an author for one or more existing books.
- Searching a book by title should succeed if the submitted title matches a part of or the full title of one or more existing books.
- Lookups of titles or authors for which we expect no match should return an empty result set.
The obvious way to go about validation is to just fill up next_state/3 callback clauses for each call in bookstore_db, stick all the checks into postconditions right there, and call it a day. The downside of this approach is that it will be difficult to gather metrics and know how many of our calls hit each of the cases, or if most attempts will hit the same case ...