Stateful Testing

Preface

The ideas implemented here are based on this article by Claessen and Hughes.

Download the framework here.

Intuitive description

Given an object with changing state, for example a linked list, hash table or a user-defined class, how do we best test it? The main idea here is to identify different sequences of operations on the object that should result in the same state. For example, consider a stack stack. The commands stack.push(A); stack.push(B); stack.pop() should result in the same state as the command stack.push(A). That is, the commands produce observationally equivalent behaviour.

To generate many cases for each pair of commands, we randomize the values used for each operation as well as the actions performed before and after these operations. In pseudo code, we test:

prefix = randomActions();
suffix = randomActions();

TestObject T1 = new TestObject();
TestObject T2 = new TestObject();

output1 = perform(T1, prefix) + perform(T1, command1) + perform(T1, suffix);
output2 = perform(T2, prefix) + perform(T2, command2) + perform(T2, suffix);

equals(T1, T2) && equals(output1, output2);

The output allows us to also compare any other observations produced other than the final state of the object, for example the peek method of a stack which outputs the top value on the stack.

The testing framework handles most of this test, you mostly need to write the code that generates command1 and command2, i.e. the commands that should produce equivalent observations.

The framework

The framework consist of two classes:

• StatefulTest: For the representation of a property, i.e. the construction of the two commands to be compared and whether they can be prefixed and/or suffixed with arbitrary commands.
• StatefulTestCase: A concrete instance of the property. These are randomly generated by the framework in order to run multiple instances of the same property described by a StatefulTest.

Robot: an example instantiation

This section discusses how to instantiate the framework for a particular object you want to test. Since this is already done for all objects used in the labs and exercises, you could just read the description of the Robot class under test and then skip to the next section. (Though reading the rest of this section might be insightful nonetheless.)

An instantiation of the framework needs to specialise these two classes to the particular object under test. As an example, we take the following class representing a robot that can move around in infinite space:

public class Robot {

  private int x_pos = 0;
  private int y_pos = 0;

  public void forward(int steps)  { y_pos = y_pos + steps; }
  public void backward(int steps) { y_pos = y_pos - steps; }
  public void left(int steps)     { x_pos = x_pos + steps; }
  public void right(int steps)    { x_pos = x_pos - steps; }
  
  /* For simplicity, we consider two robots equal if they are at the same
     location. */
  public boolean equals(Object o) {
    if (!(o instanceof Robot))
      return false;
    Robot other = (Robot) o;
    return other.x_pos == this.x_pos && other.y_pos == this.y_pos;
  }
  
  /* Inspecting the inner state of the robot. */
  public String toString() {
    return "(" + x_pos + ", " + y_pos + ")";
  }

}

In order to construct commands for the robots, we need a representation of the methods of this object. Note that this is already done for all objects used in the exercises and labs in this course.

public class RobotAction {

  public enum ActionType {
    FORWARD, BACKWARD, LEFT, RIGHT
  };

  public ActionType type;
  public Integer value;

  public RobotAction(ActionType type, Integer value) {
    this.type = type;
    this.value = value;
  }

  public String toString() {
    switch (this.type) {
    case FORWARD:
      return "forward(" + this.value + ")";
    case BACKWARD:
      // ...
    }
  }
  
  // Convenience method for end users.
  public static RobotAction newForward(int value) {
    return new RobotAction(ActionType.FORWARD, value);
  }
  
  // Similar methods for Backward, Left, Right
  // ....

}

Next we need to implement the StatefulTestCase class for robots. This class requires methods that perform the desired operations, generate sequences of random actions for possible prefix and suffix, plus some boilerplate. Again, this is already done for all objects used in the exercises and labs in this course.

// We implement the test case for the Robot class and RobotActions. The Integer
// argument, specifying the type of outputs, can be ignored for now.
public class RobotTestCase extends
    StatefulTestCase<Robot, RobotAction, Integer> {

  private Random rand = new Random();

  // Boilerplate.
  public RobotTestCase(
      StatefulTest<Robot, RobotAction, Integer> test) {
    super(test);
  }

  // Perform the requested actions on the robot, appending any outputs to the
  // provided output list.
  @Override
  public void perform(Robot robot, RobotAction action,
      LinkedList<Integer> out) {
    switch (action.type) {
    case FORWARD:
      robot.forward(action.value);  break;
    case BACKWARD:
      robot.backward(action.value); break;
    case LEFT:
      robot.left(action.value);     break;
    case RIGHT:
      robot.right(action.value);    break;
    }
  }

  // Boilerplate (for Robot).
  @Override
  public void initialize() {
  }

  // Set up the test case. We must call the method 'setObjects' to provide the
  // initial objects on which we will run both commands (and prefix, suffix).
  @Override
  public void setUp() {
    setObjects(new Robot(), new Robot());
  }

  // Generate a sequence of random actions to be used as common prefix or
  // suffix.
  @Override
  public RobotAction[] randomActions(int n) {
    RobotAction[] result = new RobotAction[n];
    for (int i = 0; i < n; i++) {
      switch (rand.nextInt(4)) {
      case 0:
        result[i] = RobotAction.newForward(rand.nextInt(20));
        break;
      case 1:
        result[i] = RobotAction.newBackward(rand.nextInt(20));
        break;
      // etc.
      }
    }
    return result;
  }
}

We also need to specify the general form of a test case. Unless we want to change any default settings, this is just a specialisation of the StatefulTest class:

public abstract class RobotTest extends
    StatefulTest<Robot, RobotAction, Integer> {
}

Writing the properties

Finally, we get to the code that actually implements the property-based tests, which is what is required of you in this course. Again, most of the framework is already created for the objects in this course:

public class RobotTestSuite {

  static Random rand = new Random();

  public static final RobotTest myTest = new RobotTest() {

    // TODO
    
  };

  /** Runs until all test are successful or a bug is found. */
  public static void runAllTests() {
    int NTEST = 1000;

    RobotTest[] tests = { myTest };

    for (RobotTest test : tests) {
      System.out.print("Testing " + test.name() + "... ");
      int i = 1;
      for (; i <= NTEST; i++) {
        RobotTestCase testCase = new RobotTestCase(test);
        if (!testCase.initializeAndRunTest()) {
          System.out.println("\nBug found after " + i + " tests:");

          testCase.minimizeContext();
          testCase.print();
          System.out.println();
          break;
        }
      }
      if (i > NTEST)
        System.out.println("OK " + NTEST + " tests.");
    }

  }

  public static void main(String[] arg) {
    runAllTests();
  }
}

The existing code runs all the tests listed in the tests variable. As you can see, it also performs some input minimalisation if a bug is found, generating a more useful bug report. The only part that remains for you to fill in is the TODO part.

As an example, we could say that moving n steps forward and then back again should have no effect on the robot.

  /* forward(n), backward(n) <==> no action */
  public static final RobotTest fwdBwd = new RobotTest() {

    public String name() {
      return "forwardBackward";
    }
    
    // This is the default but you could overwrite it.
    public boolean withPrefix() { return true; }    
    
    // This is the default but you could overwrite it.
    public boolean withSuffix() { return true; }

    // This is the function that actually dictates the property:
    public void initialize(
        StatefulTestCase<Robot, RobotAction, Integer> testCase) {
      int steps = rand.nextInt(20) + 1;
      RobotAction[] fb = new RobotAction[] {
          RobotAction.newForward(steps),
          RobotAction.newBackward(steps)
        };
      RobotAction[] nothing = new RobotAction[] { };
      
      // Important: set the commands that should result in an equal robot state:
      testCase.setCommands(fb, nothing);
    }
  };

Running the test

Simply run the RobotTestSuite. Because the robot is implemented correctly, you should see:

Testing forwardBackward... OK 1000 tests.

Now, let us introduce a bug in the robot, to see if the test finds it. We change the backward function to always take one step backward (and ignore the value of its argument):

public void backward(int steps) {
  y_pos = y_pos - 1;
}

The test suite finds a bug very quickly:

Testing forwardBackward... 
Bug found after 1 tests:
  Prefix:     []
  Suffix:     []
  Commands 1: [forward(7), backward(7)]
  Commands 2: []
  Result 1:   (0, 6)
  Result 2:   (0, 0)
  Output 1:   []
  Output 2:   []

Let's understand this bug report:

• Prefix, Suffix: The common prefix and suffix of commands shared by the commands you are comparing. They have been minimized to arrive at a simpler bug report. If you comment out the line testCase.minimizeContext(); in the function runAllTests, you can observe the original test. You can run the program several times to see that the prefix and suffix are indeed random.
• Commands 1, Commands 2: The two sequences of commands specified by the test forwardBackward. These are the commands that are being compared for demonstrating observably equivalent behaviour.
• Result 1, Result 2: The final states of the two robots after executing the common prefix, their own command and the common suffix. We can see that these states are not equal, and therefore the commands do not give equivalent observable behaviour. In this case, the first command moved the robot forward to position (0, 7), but then back only one step (due to our bug) to position (0, 6). This is the bug found by the test.
• Output 1, Output 2: Apart from the (final) state of the two objects, in general they may produce more observations while running the commands. This we will discuss next.

Dealing with outputs

Most data structures will have methods that result in intermediate observations. For example, the method pop on a stack or get on a list allows us to observe a value in the data structure.

We want to test these functions as well. First, we need to add such a function to our robot (make sure the bug we introduced previously in backward is no longer there). We will add a function that prints the Manhattan distance is from the robot to its starting position (0,0):

public int distance() {
  return Math.abs(x_pos) + Math.abs(y_pos);
}

We need to include this function in the list of robot actions. To allow us to test these functions, we also need an oracle-like "action" which outputs a pre-determined value. We will call this the OUTPUT action.

public class RobotAction {

  public enum ActionType {
    FORWARD, BACKWARD, LEFT, RIGHT, DISTANCE, OUTPUT
  };
  
  // ...

  // The distance function takes no value.
  public static RobotAction newDistance() {
    return new RobotAction(ActionType.DISTANCE, 0);
  }

  public static RobotAction newOutput(int value) {
    return new RobotAction(ActionType.OUTPUT, value);
  }
}

The test case needs to be extended to understand these two new actions. This is what we use the list of outputs for:

public class RobotTestCase extends
    StatefulTestCase {

  // ...

  // Perform the requested actions on the robot, appending any outputs to the
  // provided output list.
  @Override
  public void perform(Robot robot, RobotAction action, LinkedList<Integer> out) {
    switch (action.type) {

    // ...

    case DISTANCE:
      out.add(robot.distance());
      break;
    case OUTPUT:
      out.add(action.value);
      break;
    }
  }

  // ...
}

Since the distance function does not change the state of the robot, we do not include it in the function randomActions to generate the prefix and suffix.

We can now add a test for the distance function. Note that we can only predict what the returned value of this function should be if we know the starting point. We therefore specify that there should be no random prefix of commands:

/* backward(n), distance(), forward(n) <==> output(n) */
public static final RobotTest simpleDistance = new RobotTest() {

    public String name() {
      return "simpleDistance";
    }

    public boolean withPrefix() {
      return false;
    }

    // This is the function that actually dictates the property:
    public void initialize(
        StatefulTestCase testCase) {
        
      int steps = rand.nextInt(20) + 1;
      
      RobotAction[] distance = new RobotAction[] {
          RobotAction.newBackward(steps),
          RobotAction.newDistance(),
          RobotAction.newForward(steps) };
          
      RobotAction[] output = new RobotAction[] {
          RobotAction.newOutput(steps) };
          
      testCase.setCommands(distance, output);
    }
};

Don't forget to add the simpleDistance test to tests in the runAllTests function. If you followed all instructions correctly, you will now see the following when running the test suite:

Testing forwardBackward... OK 1000 tests.
Testing simpleDistance... OK 1000 tests.

However, if we had a bug in the distance function:

public int distance() {
  return x_pos + y_pos;
}

We would find that although the final state (Result) of both robots is equal, the intermediate observations are not:

Testing forwardBackward... OK 1000 tests.
Testing simpleDistance... 
Bug found after 1 tests:
  Suffix:     []
  Commands 1: [backward(5), distance(), forward(5)]
  Commands 2: [output(5)]
  Result 1:   (0, 0)
  Result 2:   (0, 0)
  Output 1:   [-5]
  Output 2:   [5]

Keep on testing

The tests we included were rather simple. Try to come up with more properties that should hold on the robot, or extend the robot with more methods, e.g.:

• Test the left and right functions.
• Test the distance function with the robot making more interesting movements then just backwards.
• Add a function void teleport(int x, int y) which teleports the robot to the specified location.
• Add a function int pathLength() which returns the length of the path the robot has travelled.
• Introduce bugs and see if your tests find them.