Testing Stateful S7 Protocols
In s7contract: Behavioral Contracts and Generative Laws for 'S7'

knitr::opts_chunk$set(collapse = TRUE, comment = "#>")
knitr::read_chunk(
  system.file("examples", "store-laws.R", package = "s7contract")
)

A mutable store must behave correctly across calls: a put changes a later get, a delete removes a key, and a reset clears earlier entries. We can test these relationships by generating sequential commands and comparing each operation with a reference model.

The protocol and its implementations

This protocol stores one integer per string key and reports keys in sorted order. The example uses bounded strings and small integer values. Missing keys return NULL; generated get and delete commands use existing keys.

One implementation stores environment bindings; the other updates a list held in an environment. Both use ordinary S7 methods.

Commands and a reference model

Keys contain one to four code points from a, b, c, and \u00e9 (é). This recipe converts the alphabet to UTF-8, rejects missing and byte strings, and counts code points rather than bytes or grapheme clusters. The alphabet must be nonempty; each entry must contain exactly one code point. With min = 0, the recipe also generates "", which environment bindings cannot use as a key. Shrinking removes chunks before moving characters toward earlier alphabet entries.

paste() preserves UTF-8 here and collapses zero entries to one empty string. Missing values are rejected before concatenation because paste() would turn them into the literal text "NA".

The model is a named list of expected values. Each command defines its input generator, implementation call, and postcondition. A model update derives the next state from the input. get and delete are available only when a key exists; their preconditions also apply during shrinking.

ensure(state, input, output) sees the model before the command and returns a scalar logical. It runs after update() has computed the next model. The model's expected values come from the inputs, independently of the store's answers.

One law, two fixtures

new_state_law() gives every case and evaluated shrink a fresh fixture. Teardown runs once after each successful setup, including after a false postcondition, warning, or error.

Sequence length grows with the runner's size, up to max_commands. Generation may stop sooner when no command is available. Empty sequences are allowed. expect_law() can run the same law as one tinytest expectation.

The classifier records sequences containing multi-character and non-ASCII put keys. It counts generated inputs, including any suffix after an execution failure.

A put that truncates keys

This implementation keeps only the first character when writing a key. The law reduces its failure to put("aa", 0L): a subsequent get of "aa" returns NULL.

A reset that leaves data behind

This subclass has every required method, but reset does nothing:

The runner reduces the failure to a put followed by a reset. It first removes chunks of commands, then shrinks their inputs. After each change, it removes commands whose preconditions no longer hold, along with their dependents. The search retains failures of the same command's postcondition; the result is minimal relative to the shrink tree and evaluation budget.

The failure condition retains the resolved inputs, outputs, and model states:

The original trace is in store_failure@counterexample@original_condition$trace. Unexpected callback errors stop shrinking and preserve an established counterexample. If teardown also fails, its condition is retained separately as cleanup_condition. shrink_condition reports why the search stopped.

Replay requires unchanged commands, generators, run parameters, and compatible R/package versions. Setup must reproduce the initial state; shared mutable state outside the fixture would break that guarantee. The runner restores the caller's RNG state as described in Generative Laws with tinytest.

Commands that return handles

Some protocols allocate a handle that later commands consume. During generation, update(state, input, output) receives an opaque reference to the future output. It can append that reference to a list of live handles, and later generators can select one with gen_element(). During execution, the same update receives the actual handle.

References resolve when passed directly as command inputs or nested in ordinary lists. They retain the producer's ID when earlier commands are removed. Removing a producer also removes consumers of its output. References inside classed containers are not traversed; place them in a plain list before execution. The update must work with both symbolic and concrete outputs, without inspecting their representation. Models need value semantics; traces containing mutable handles retain R's reference semantics.

The design follows R Hedgehog's state-machine example and Haskell Hedgehog's commands. For the model-based testing background, see Hughes (2016). This runner executes sequential commands; it does not test concurrent histories.