Testing, Debugging, and Verification TDA567/DIT082, LP2, HT2017



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 queue q. The commands q.add(A); q.add(B); q.remove() should result in the same state as the command q.add(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 front method of a queue which outputs the top value on the queue.

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 packages:

  • se.chalmers.tdv.testing: This package contains the classes used to describe the test cases, and how to run them.

    • Property.java: This file is used to describe both command1 and command2, and if the test case including these commands will also include a prefix and suffix, or not.
    • Interpreter.java: Interface whose implementation will execute the actions (i.e., sequence of commands) decribed on a test case.
    • TestCase.java: This file describes the test cases. Note that test cases will be generated from properties, i.e., from objects of the class Property. Below we provide an example on how this is done.
    • TestRunner.java: This class represents the evaluation of the test cases, i.e., implements the algorithm described above (in pseudo code).

  • se.chalmers.tdv.minimize: This package contains a (generic) implementation of the DDMin algorithm, and several classes with useful methods for describing the tests cases. DDMin is used in the class TestRunner to shrink the prefixes ans suffixes of the failing test cases.

Robots: 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 actions (i.e., sequence of commands) for the robots, we need a representation of the methods of this object.

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:
      return "backward(" + this.value + ")";
    // ...
    }
  }
  
  // Method used to generate random prefixes and suffixes.
  public static RobotAction[] randomActions(int n) {
     QueueAction[] result = new QueueAction[n];
     Random rand = new Random();
     for (int i = 0; i < n; i++) {
         switch (rand.nextInt(3)) {
           case 0:
                  result[i] = new RobotAction(ActionType.FORWARD,rand.nextInt(20));
                  break;
           case 1:
                 result[i] = new RobotAction(ActionType.BACKWARD,rand.nextInt(20));
                 break;
           //.....
      }
      return result;
  }

}

Next, we need to implement an interpreter for these actions.

public class RobotInterpret implements 
    Interpreter<RobotAction, Tuple<Robot,ArrayList<Integer>>> {
	
  public RobotInterpret() { }

  // Performs the requested actions on the robot, appending any outputs to the
  // provided output list.
  @Override
  public Tuple> interpret(RobotAction[] actions) {
    Robot robot = new Robot();
    ArrayList out = new ArrayList<>();
    for(RobotAction action : actions){
        switch (action.type) {
            case FORWARD:
                 out.add(robot.forward(action.value));
                 break;
            case BACKWARD:
                 out.add(robot.backward(action.value));
                 break;
            case LEFT:
                 out.add(robot.left(action.value));
                 break;
            case RIGHT:
                 out.add(robot.right(action.value));
                 break;
        }
    }
    return new Tuple>(robot, out);
  }
  //....
}

Finally, we can proceed to describe a test suite for testing the class Robot. This the code actually implements the property-based tests, which is what is required of you in this course.

public class RobotTestSuite {
  // set this to true to generate code to past into a file to use the debugger
  static final boolean PRINT_CODE = false;

  /** Length of the randomly generated prefixes and suffixes. */
  static final int MAX_PREFIX_LENGTH = 10;
  static final int MAX_POSTFIX_LENGTH = 10;

  /** Max number of generated test cases. */
  static final int MAX_NR_TESTS = 10000;

  /** Value to use on the actions. */
  static Integer A = 10;

  // Action generator methods. 
  public static RobotAction forward(Integer value) {
     return new RobotAction(ActionType.FORWARD, value);
  }
  public static RobotAction backward(Integer value) {
     return new RobotAction(ActionType.BACKWARD, value);
  }
  public static RobotAction right(Integer value) {
     return new RobotAction(ActionType.RIGHT, value);
  }
  public static RobotAction left(Integer value) {
     return new RobotAction(ActionType.LEFT, value);
  }

  /** Definition of the actions. */
  /* forward(n), backward(n) <==> no action */
  static final Property forwardBackward =  new Property<>("forwardBackward", true, true, 
      new RobotAction[]{ forward(A), backward(A)}, 
      new RobotAction[]{ });

  /** Array of commands to use on the generation of test cases. */
  static final Object[] allPropertiesObjects = new Object[]
      { forwardBackward };
 
  static final Property[] allProperties;
	
  static {
      allProperties = (Property[]) Array.newInstance(Property.class, allPropertiesObjects.length);
      for(int i = 0 ; i < allProperties.length; i++){
          allProperties[i] = (Property) allPropertiesObjects[i];
      }
  }

  /** Generates the test cases from the properties. */
  static TestCase generate(Property property){
     RobotAction[] prefix  = property.prefix ? RobotAction.randomActions(MAX_PREFIX_LENGTH)   : new RobotAction[]{};
     RobotAction[] postfix = property.postfix ? RobotAction.randomActions(MAX_POSTFIX_LENGTH) : new RobotAction[]{};
     return new TestCase<>(prefix, property.commandsLeft, property.commandsRight, postfix);
  }

  /** Runs until all test are successful or a bug is found. */	
  static void runTest(Property property){
      Random rand = new Random();
		
      System.out.println("Testing property: " + property.name);
      for(int i = 0 ; i < MAX_NR_TESTS; i++){
          int queueSize = rand.nextInt(MAX_QUEUE_SIZE) + 1;
          TestRunner>> runner = new TestRunner<>(RobotAction.class,new RobotInterpret());
          A = new Integer(rand.nextInt(MAX_RANDOM_INT));
          if(!runner.runTestPrint(PRINT_CODE,generate(property))){
              return;
          }
      }
      System.out.println(MAX_NR_TESTS + " test succeeded");
  }
  
  static void runAllTests() {
      for(Property prop : allProperties){
        if(prop!=null){
           runTest(prop);
        }
      }
  }
	
  public static void main(String[] args){
     runAllTests();
  }
}

The existing code generates tests to analysed all the actions listed in the allProperties variable. As you can see, it also performs some input minimalisation if a bug is found, generating a more useful bug report. As an example, we could say that moving n steps forward and then back again should have no effect on the robot, as it is described in property forwardBackward. Again,

/** Definition of actions. */
  /* forward(n), backward(n) <==> no action */
  static final Property forwardBackward =  new Property<>("forwardBackward", true, true, 
      new RobotAction[]{ forward(A), backward(A)}, 
      new RobotAction[]{ });

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 property: forwardBackward
Bug found! Shrinking ...
  Prefix:     []
  Commands 1: [forward(7), backward(7)]
  Commands 2: []
  Suffix:     []
  Result 1:   {(0, 6),[]}
  Result 2:   {(0, 0),[]}

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 first component corresponds to 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. The second component corresponds to observations which may be produced while running the commands.



Home | Course | Schedule | Exam | Exercises | Labs | Evaluation | Tools Atze van der Ploeg, Dec 2, 2016