Business Logic
We use TLA+ to find flaws in our designs. But there’s another, subtler benefit: we also find places where the spec is ambiguous. Formally specifying your problem forces you to decide what you actually want out of your system. This is especially important
- PDF / 195,421 Bytes
- 18 Pages / 504 x 720 pts Page_size
- 106 Downloads / 298 Views
Business Logic We use TLA+ to find flaws in our designs. But there’s another, subtler benefit: we also find places where the spec is ambiguous. Formally specifying your problem forces you to decide what you actually want out of your system. This is especially important when we model “business logic,” features, and requirements. To work through this, we’ll use TLA+ to spec a simple library system and show how the act of specifying can itself find faults in the spec. In our system, people should be able to check out books, renew books, and return them. They will also be able to reserve books: a reserved book cannot be checked out by anybody else. The system should be internally consistent (all books are accounted for), and anybody who wants a book should eventually be able to check it out. Most of these seem like simple features, but how they interact can lead to surprising behavior. In addition to the final specs, I’ll be showing the development process and the dead ends we can run into. This is an example of how we write specifications and would be incomplete without it.
The Requirements We begin with the standard setup, extensions and constants. There seem to be two constants here: one that represents the set of books and one that represents the set of people. ---- MODULE main ---EXTENDS Integers, TLC, Sequences CONSTANTS Books, People PT == INSTANCE PT ====
© Hillel Wayne 2018 H. Wayne, Practical TLA+, https://doi.org/10.1007/978-1-4842-3829-5_10
149
Chapter 10
Business Logic
On second thought, though, “books” is ambiguous. Are we going to assume we’re only looking at one type of book or multiple types? If we do one type the spec will be simpler and probably check faster, and if we do multiple types the spec will more closely mirror our problem domain. I decide to go with the latter. Since the library’s holdings will change over time, we might assign that to a variable. (*--algorithm library variables library = \* ??? end algorithm; *) Question two: Do we have a single copy of each book, or can we have multiple copies? In the former case, we can make library a set. In the latter case, we actually want it to be a map of books to numbers, something like [Books -> Nat]. Again, the second case is closer to what an actual library has. That means we have to introduce another constant for the range of possible copies. We can still test the model with one copy of each book by setting that range to {1}. CONSTANTS Books, People, NumCopies ASSUME NumCopies \subseteq Nat (*--algorithm library variables library \in [Books -> NumCopies]; end algorithm; *) For each person, we’ll give them the ability to take a book from the library or return a book to the library. They have a private books variable that tracks what they have, a Checkout action, and a Return action. process person \in People variables books = \* ??? begin Person: either \* Checkout skip; 150
Chapter 10
Business Logic
or \* Return skip; end either; goto Person; end process; And again, we have a question:
Data Loading...
