Guide & Tutorial

Lost in Translation

Writing software often feels like an act of translation. Stories, requirements, and specifications must be translated into working code. Some programming languages have types to add a bit of "crispness" (thanks Simon-Peyton Jones) to the translation. While a variety of interesting properties can captured in types, often types are used in a provincial manner - they provide confidence to the programmer but the value to other stakeholders remains difficult to prove. Dynamic languages Clojure offer a different approach in the form ofclojure.spec, but somehow an artisanal odor persists.

Irrespective of their professed beliefs in typing disciplines, a good number of programmers embrace some form of unit testing. The spirit of Test Driven Development contains a pearl of common sense - it's probably a good idea to think about what we want before we go asking for trouble. Yet, as software systems grow in complexity and age inexorably into some high level enemy in Elden Ring, what value do unit tests give us in following the larger plot? Picking any old random unit test does not give us fractal view, rather only the end state of some Game of Life. Like a monthly receipt of JS Bach's expenses, it gives a sense how the person lived, but not much clarification into how the results were achieved.

Documentation and diagrams fulfill important roles as satellite photographs, but given must of us are employed as architects and engineers and not Cold War spies, we need something more tanglible such as a scale model to ignite our reason.

A Motivating Example

Often stateful property based testing tutorials uses data structures as a motivating example. Unfortunately this is akin teaching people to write via the poems of Emily Dickinson.

A great many software systems are stateful system with uncoordinated users. A user may take various actions but often those actions are limited or expanded based on previous actions taken. So we will start here.

Thinking about models

Imagine we have a long lived production system and that we would like to gain some reasoning power over this system. From this vantage point details like programming language, database technology, user interace matter very little. We simply want to document how we believe a portion of the system works.

To keep the tutorial short let's imagine the following set of requirements:

1. There are two users, User A and User B
2. There are two rooms, Room 1 and Room 2
3. There is a key
4. Between the two rooms there is a door
5. The door may be open, closed, or locked
6. Either user can take the key if they are in the room where it lies
7. Once the key is taken by a user it cannot be taken by the other user
8. A user in possession of the keym may drop the key
9. A user in possession of the key can unlock the door
10. Any user can open an unlocked door regardless of the room they are in
11. Any user can close an open door regardless of the room they are in
12. Any user in possession of the key can lock a closed door

While this may seem like a lot requirements, we'll see how to encode this in a little over a hundred lines, and then see how we can generate as many valid sequences of steps for the model as we like. Finally we can apply this tool to a faux legacy system and the model can give ys minimal sequence for which some requirement is violated.

Defining an initial state

Since we are in a purely symbolic realm we can define the state in as straightforward manner as possible. The point is to capture our understanding of the system, implementation details are beside the point - a proper tool for thinking.

Here is one possible representation:

(def init-state
  {:user-a  #{}
   :user-b  #{}
   :door    :locked
   :room-1  #{:key :user-a :user-b}
   :room-2  #{}})

This emphasizes examinability - who has the key, what room are the users in, and what is the door state.

Defining the model

This is our model. These are possible events that can occur and it's extremely easy map this back to our expecadtions about a working system. We not going to examine all of the command specs, just a few to get a feel for the practice of writing models:

(def model
  {:open      open-spec
   :close     close-spec
   :lock      lock-spec
   :unlock    unlock-spec
   :take-key  take-key-spec
   :drop-key  drop-key-spec
   :move      move-spec})

Defining a command spec

Given the above initial state, it should be clear only one action is possible - someone has to take the key. So let's start with take-key-spec:

(def take-key-spec
  {:run?       user-and-key-in-same-room?
   :args       (fn [state]
                 (gen/tuple
                   (gen/elements
                     (disj (get state (room-with-key state)) :key))))
   :next-state (fn [state {:keys [args]}]
                 (let [user (first args)]
                   (-> state
                     (update user conj :key)
                     (update (user->room state user) disj :key))))
   :valid?     (fn [state {[user] :args}]
                 (= (user->room state user)
                    (room-with-key state)))})

The first question to ask is whether a command is available to chosen. This is the job of :run?. This function will take the current value of the state and examine it and either return true or false. In this case a user can take the key only if they are both in the same room.

We will talk about :args last, it involves clojure.test.check.generators which are scarier than they sound.

So let's move on to :next-state. This function take the current state and the command that was generated along with the realized :args. This is the information we need to update the state. In this case we move the key to the user and remove the key from the room.

:valid? at first glance might seem strange. But need only realize that during shrinking (when we are searching for a minimal case), commands before us might get dropped. If for example the other user had just dropped the key but command gets dropped, then we can no longer pick it up. So this function take state and the commannd and determines whether during shrinking we are still valid.

Finally :args. We need to use use clojure.test.check.generators to create arguments. If we much choose between a few options we use gen/elements. We wrap this in gen/tuple because that's natural - arguments are sequential. Later this will be convenient.

That's it! Let's look at drop-key-spec next.