stateful-check

A Clojure library designed to help with testing stateful systems with test.check.

Example

As an example, let’s implement a simple mutable queue and a specification to test it.

To begin with, let’s pull in the dependencies we’ll need later.

(ns stateful-check.example
  (:require [clojure.test :refer [is]]
            [clojure.test.check.generators :as gen]
            [stateful-check.core :refer [specification-correct?]]))

Queue implementation

For our queue, let’s just wrap a clojure.lang.PersistentQueue in an atom, and have our push/pop operations act on one of these atoms.

(defn new-queue []
  (atom clojure.lang.PersistentQueue/EMPTY))
(defn push-queue [queue value]
  (swap! queue conj value))
(defn pop-queue [queue]
  (swap! queue pop))

There we go, easy! Now, let’s write some specifications for the push/pop operations (we’ll treat new-queue as a setup operation, so we don’t need a specification for it).

For the following commands we’re going to model the state of the real queue by a vector under the key :elements in the state. We’ll conj onto the end of the vector to model calling push-queue, and we’ll (comp vec next) to remove the element at the front of the vector to model calling pop-queue.

Command: push-queue

Let’s start with push-queue:

(def push-queue-specification
  {:model/args (fn [state]
                 [(:queue state) gen/nat])
   :real/command #'push-queue
   :next-state (fn [state [_ val] _]
                 (update-in state [:elements] conj val))})

This specification tells the system how to generate arguments for this command, how to run the command, and what the expected effect on the state of the system is. In this case, we expect our command to take the queue under test and a natural number and we expect it to add that number to the end of the :elements collection (which will be a vector) in the state.

Command: pop-queue

Now how about pop-queue?

(def pop-queue-specification
  {:model/requires (fn [state]
                     (seq (:elements state)))
   :model/args (fn [state]
                 [(:queue state)])
   :real/command #'pop-queue
   :next-state (fn [state _ _]
                 (update-in state [:elements] (comp vec next)))
   :real/postcondition (fn [prev-state _ _ val]
                         (= (-> prev-state :elements first)
                            val))})

This command specification specifies that we expect pop to modify the state by removing the first element from the :elements collection (leaving it as a vector). The postcondition then asserts that the result of the command must be equal to the first element from the old :elements collection (so we pop off the front).

Specification: queue-spec

Now we have a specification for our two commands, let’s put them together in a system specification.

(def queue-spec
  {:commands {:push #'push-queue-specification
              :pop #'pop-queue-specification}
   :real/setup #'new-queue
   :initial-state (fn [queue] {:queue queue, :elements []})})

This system specification tells the system how to run our command specifications. It specifies the initial state of the system, which our other commands then rely on (ie. the :queue and :elements keys are used by our command specifications).

We can now run this specification with:

(is (specification-correct? queue-spec))
;;
;; FAIL in clojure.lang.PersistentList$EmptyList@1 (form-init3821556149176680553.clj:1)
;;    #<1> = (:push #<setup> 0)         => #<PersistentQueue clojure.lang.PersistentQueue@1f>
;;    #<2> = (:pop #<setup>)    => #<PersistentQueue clojure.lang.PersistentQueue@1>
;; Error while checking postcondition
;; Seed:  1417059242645
;; Visited:  6
;;
;; expected: :pass
;;   actual: :fail

Oh no! Our test has failed! We’ve got a nice print-out of what commands can be executed to provoke this failure, and what values were seen during the actual failed execution.

As we can see, our queue fails when we :push zero, then :pop. If we look at the output of the :pop command we can see that the value it’s returned isn’t at all what we expected! We expected it to return 0, because that’s what we pushed into the queue. Instead, it’s returned a queue object! Our pop-queue function is quite broken.

Let’s fix it:

(defn pop-queue [queue]
  (let [value (peek @queue)]
    (swap! queue pop)
    value))

Now we can try re-running out tests:

(is (specification-correct? queue-spec))

No output? That’s a success!

Specifications

For a detailed description of how a stateful-check specification has to be structured, see the specification document.

Related work

• test.check (generative testing for Clojure)
• QuviQ Quickcheck (commercial generative testing for Erlang)
• PropEr (open source generative testing for Erlang)

Future work

• race-condition debugging (parallel test cases)

License

Copyright © 2014 Carlo Zancanaro

Distributed under the Eclipse Public License either version 1.0 or (at your option) any later version.