The last episode was about patterns to find good properties. One pattern I mentioned there is Stateful Testing. Some PBT proponents treat this one with some condescension since state is considered as something that should be avoided - at least in functional programming. I tend to look at it with more tolerance.

Stateful TestingPermalink

I agree with the general notion of trying to get away from state if you reasonably can, but sometimes the stateless implementation of an algorithm feels weired - especially when working in a language like Java, in which some functional constructs require a lot of additional boilerplate. In other situations a state machine is at the heart of a domain problem and you won’t get away without state in one form or another. Those are the times when properties to test the expected behaviour of a state machine come in very handy. Let’s look at a simple example: a stack.

Our stack is supposed to handle only strings, so the interface is simple and probably obvious:

public class MyStringStack {
	public void push(String element) { ... }

	public String pop() { ... }

	public void clear() { ... }

	public boolean isEmpty() { ... }

	public int size() { ... }

	public String top() { ... }
}

Finite State MachinesPermalink

As any object with state, a stack can be considered to be a finite state machine which comes with a few characteristics:

1. It always has a defined current state - out of a finite list of possible states.
2. For every state there is a finite and possible empty list of transitions that bring the state machine into its next state.
3. Transitions are often triggered by actions (aka events).

One way to represent a state machine is a state transition table. Here’s one for MyStringStack:

Current State Action Next State empty push filled empty clear empty filled push filled filled(1) pop empty filled(1+) pop filled filled clear empty

This table reveals a few things:

• It can give us a hint about what transitions we might want to test.
• Not all actions are allowed in all states, e.g. pop does not make sense for an empty stack.
• A stack has additional and important functional properties that are not visible in the transition table, e.g. pop should always return the last element that was pushed on the stack. Those functional properties can typically be considered as postconditions or invariants.

Looking at this from a property-based testing point of view the following approach seems viable:

1. Generate a random sequence of actions.
2. Apply this sequence to a state machine in its initial state.
3. For any (allowed) action, check that the resulting state is correct and that any other invariants and postconditions hold.

With some imagination you should be able to implement this approach using just jqwik’s basic mechanisms. It’s easier, however, to leverage the library’s built-in support for state testing. There’s two things you have to do:

1. Define a state machine’s possible actions
2. Formulate property to execute the state machine

Defining the ActionsPermalink

Actions have to implement the Action interface:

public interface Action<M> {

	default boolean precondition(M model) {
		return true;
	}

	M run(M model);
}

The precondition method is only required for actions that are not always allowed, e.g. pop. The run method does not only apply an action to a model but it should also check all postconditions of an action, including the new state.

For convenience I’ll put all action definitions into a single container class:

class MyStringStackActions {

	static Arbitrary<Action<MyStringStack>> actions() {
		return Arbitraries.oneOf(push(), clear(), pop());
	}

	static Arbitrary<Action<MyStringStack>> push() {
		return Arbitraries.strings().alpha().ofLength(5).map(PushAction::new);
	}

	private static Arbitrary<Action<MyStringStack>> clear() {
		return Arbitraries.constant(new ClearAction());
	}

	private static Arbitrary<Action<MyStringStack>> pop() {
		return Arbitraries.constant(new PopAction());
	}

	private static class PushAction implements Action<MyStringStack> {

		private final String element;

		private PushAction(String element) {
			this.element = element;
		}

		@Override
		public MyStringStack run(MyStringStack model) {
			int sizeBefore = model.size();
			model.push(element);
			Assertions.assertThat(model.isEmpty()).isFalse();
			Assertions.assertThat(model.size()).isEqualTo(sizeBefore + 1);
			Assertions.assertThat(model.top()).isEqualTo(element);
			return model;
		}

		@Override
		public String toString() {
			return String.format("push(%s)", element);
		}
	}

	private static class ClearAction implements Action<MyStringStack> {

		@Override
		public MyStringStack run(MyStringStack model) {
			model.clear();
			Assertions.assertThat(model.isEmpty()).isTrue();
			return model;
		}

		@Override
		public String toString() {
			return "clear";
		}
	}

	private static class PopAction implements Action<MyStringStack> {

		@Override
		public boolean precondition(MyStringStack model) {
			return !model.isEmpty();
		}

		@Override
		public MyStringStack run(MyStringStack model) {
			int sizeBefore = model.size();
			String topBefore = model.top();

			String popped = model.pop();
			Assertions.assertThat(popped).isEqualTo(topBefore);
			Assertions.assertThat(model.size()).isEqualTo(sizeBefore - 1);

			return model;
		}

		@Override
		public String toString() {
			return "pop";
		}
	}
}

This class contains both, the action implementations and methods to create the necessary Arbitrary<Action<MyStringStack>> instances for those actions. From the outside only the static actions() method is relevant because it will be used to generate sequences.

Formulate the PropertyPermalink

The basic property test is rather straightforward:

@Property
void checkMyStackMachine(@ForAll("sequences") ActionSequence<MyStringStack> sequence) {
    sequence.run(new MyStringStack());
}

@Provide
Arbitrary<ActionSequence<MyStringStack>> sequences() {
    return Arbitraries.sequences(MyStringStackActions.actions());
}

The ActionSequence interface is part of jqwik and therefore the library knows how to create sequences - given a method to generate actions -, how to apply a sequence to a model, and how to shrink a sequence if a failing example has been found.

If we wanted to we could have additional properties, e.g. for running sequences against other intial states or with added invariants.

Running the PropertyPermalink

Let’s inject a bug into the stack implementation by disabling clear if the stack contains more than 3 elements:

public class MyStringStack...
	private final List<String> elements = new ArrayList<>();

	public void push(String element) {
		elements.add(0, element);
	}

	public String pop() {
		return elements.remove(0);
	}

	public void clear() {
		if (elements.size() < 4) elements.clear();
	}

Running the property will indeed give the result we’d expect:

org.opentest4j.AssertionFailedError: Run failed after following actions:
    push(AAAAA)
    push(AAAAA)
    push(AAAAA)
    push(AAAAA)
    clear
  final state: [AAAAA, AAAAA, AAAAA, AAAAA]
expected:<[[]]> but was:<[[AAAAA, AAAAA, AAAAA, AAAAA]]>

You find the complete example code here

Further Aspects of Stateful PropertiesPermalink

• Since Action.run(M model) is supposed to return the model in its new state the approach works perfectly fine for immutable models.

• In the example above the model can be the stack implementation itself since the MyStringStack contains everything required for executing and checking. In other situation you might have to implement a model explicitly for testing purposes. This approach is called model-based testing.

• State properties can also be used in integration testing. Consider a RESTful API that exposed some state. Actions might consist of sending out certain types of http requests. PBT will probably come up with sequences of requests that you’d never think of yourself and thereby stress your API in a different way than hand-made integrated tests do. One caveat, though: Running hundreds or thousands of tests over a network might take a very long time!

• Some PBT frameworks also allow the concurrent execution of actions in a “sequence”. That way you might be able to detect some concurrency-related bugs; what you will loose is repeatability.

Next EpisodePermalink

In the next article I will show in an example how Test-Driven Development and Property-Based testing can work well together.