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

Exercises week 2 - Specifications, Testing

You can download test cases for exercise sessions 1, 2, 3 and 5 here. The test cases satisfy statement and branch coverage, but are otherwise minimal. They are produced under Eclipse and can be easily imported there if desired (File -> Import; Existing projects into workspace; Select archive file;).

Below we provide some solution notes to all exercises. Answers to questions that ask you to write specifications or to derive test cases from specifications should just be seen as possible examples, and not be taken too strictly.

There are two extremes to specification: overspecification (when you disclose too much information about how things are implemented) and underspecification (being too vague on what the thing you are specifying does). What should drive you is mainly common sense. There can be different specifications to a method: whether they are good or not is a matter of context, and you should apply Occam's razor in order to guarantee precision and freedom for the implementors as well.

Exercise 1

Consider this method:

  public static Object[] reverse(Object[] a) {
    if (a == null) return null;
    Object[] b = new Object[a.length];
    for (int i = 0; i < a.length; i++) {
      b[i] = a[a.length - 1 - i];
    return b;

The method returns a new array where the order of the elements has been reversed. (Your specification should be more detailed than the previous sentence.)

1 a) What does this method do? Write it in a meaningful way, taking as example the slides about specification of the intro slides of the course.

specification for method reverse
  a is unchanged
    null if a is null,
    otherwise an array of the same length n as a in which
      for all elements at index i it is equal (even identical) to a[n-1-i]


  • Types don't change, therefore there is no need to enforce in the specification that what you have remains of the same type
  • The length of the input array does not change after the method returns, i.e. it has not to be ensured in the postcondition. In the case of Java, any assignment to a method's formal parameters does not change the actual parameters (because of how Java treats argument passing -- "call by value"). In the case of the array, then, the only thing that can change are the elements of the array, but not the array itself. (The same applies to any object: only its fields can be changed)
  • The specification could also be divided in two separate contracts:
    specification for method reverse
      a is null
      returns null


      a is not null
      a is unchanged
        an array of the same length n as a in which
          for all elements at index i it is equal (even identical) to a[n-1-i]

1 b) Derive test cases which together have full statement coverage. Then add test cases if necessary to have full branch coverage.

Statement coverage:

  • a = null -- executes the then-part of the if statement. Result should be null.
  • a = new Object[] { new Object() } -- array of size 1; executes the rest of the method (including the body of the loop). Result should be the same as a.

Branch coverage: The statement covering test cases also do full branch coverage (the second test case both enters and exits the for-loop).


  • If each if/else statement has statements in both its then- and else-branch, statement coverage implies branch coverage. If one of the branches is empty, statement coverage does not imply branch coverage, such as:
    if(condition) {

Exercise 2

Consider this method:

  public static void vector_add(Float[] a, Float[] b) {
    for (int i = 0; i < a.length; i++) {
      a[i] += b[i];

The method computes the vector addition of a and b and stores the result in a.

2 a) What does this method do? Write it in a meaningful way, taking as example the slides about specification of the intro slides of the course. (or see the example in exercise 4).

specification for method add
  a and b are non-null and with non-null elements,
  the length of a and b is the same,
  a and b are different objects.
  when the method returns each index i in a and b,
    a[i] is equal to the sum of a[i] and b[i] before the method was called,
    and b is unchanged


  • A possible precondition is that we can also say that a.length <= b.length. The choice is made mainly on what you would expect the user to use the piece of software, but both are correct.

2 b) Derive test cases for the method.

The specification does not contain any case distinctions; we can only distinguish between empty and non-empty arrays. This is what is called an implicit disjunction in the specification. The precondition rules out the cases in which the arguments have different lengths; therefore we could partition the input between zero length arrays, and a couple of non-zero length arrays (without null elements):

  • vector_add(new Float[]{}, new Float[]{})
    Expected result: a={},b={} -- a and b have length 0
  • vector_add(new Float[]{2.0f}, new Float[]{3.5f})
    Expected result: a={5.5f}, b = {3.5f} -- a and b have length greater than 0
  • ... more tests can be added

Exercise 3

This exercise is about an implementation of a queue. We do this using the usual "rotating array" implementation. Furthermore, we are going to stress the fact that whether testing is successful or not depends on what we expect. Consider the following class for representing a queue:

  public class Queue {
    Object[] arr;
    int size;
    int first;
    int last;

    public Queue(int max) {
      arr = new Object[max];
      size = 0;
      first = 0;
      last = 0;

    public int size() {
      return size;

    public int max() {
      return arr.length;

    public void enqueue(Object x) {
      arr[last] = x;
      if (last == arr.length) last = 0;

    public Object dequeue() {
      if (size == 0) return null;
      Object x = arr[first];
      if (first == arr.length) first = 0;
      return x;

3 a) For each method in Queue, give a specification like in points 1a and 2a.

The specifications do not give full technical details of how the state of the instance changes. They only talk about how size changes. But in addition to that they say what happens in terms of a queue. That is the so called "model based specification" where the specifications are expressed by saying how a model of the class is modified. When doing formal specifications, model based specifications are often good to use. It is then required to formally define how a class instance translates to an instance of the model. That is, this allows implementations of this specification to vary, as long as they specify the mapping between the implementation and the model assumed by users of the class.

specification for constructor Queue
   max >= 0
  internal state represents an empty queue (size = 0)
specification for method size
  returns the length of the queue (size); the state of this instance is unchanged.
specification for method max
  returns the maximum capacity of the queue
specification for method enqueue
  queue is not yet full (size < length of arr)
  x is added to the queue (size increased by one)
specification for method dequeue
  if queue is empty (size = 0) then returns null,
  otherwise removes an object from the queue (size decreases by one) and returns that removed object

In a more formal specification the specifier would have to express formally what changes to last, first and size in detail, making explicit how the specification maps to the implementation.

3 b) Derive test cases for each method. Analyse the failed tests and their relationship to what you were expecting.

Since the specifications of the method are not too detailed, from size we can indentify the following distinctions:
  • (A) 0 = size = length of arr
  • (B) 0 = size < length of arr
  • (C) 0 < size < length of arr
  • (D) 0 < size = length of arr
The letters will be referred to in the test cases below. nstead of referring to the fields of the class instance, below we express the state using the model of the class, e.g. st={7,9} means that the state correspond to the queue with the objects 7 and 9 and for which 7 will be dequeued before 9. Integers are used as objects in the queue.

Test cases for constructor:
q = new Queue(0) -> q={} (max = 0, A)
q = new Queue(5) -> q={} (max > 0, B)

Test cases for method size:
q = new Queue(0), q.size() -> 0, q={} (queue empty, A)
q = new Queue(2), q.size() -> 0, q={} (queue empty, B)
q = new Queue(2), q.enqueue(7), q.size() -> 1, q={7} (queue nonempty, C)
q = new Queue(1), q.enqueue(9), q.size() -> 1, q={9} (queue nonempty, D)

Test cases for method enqueue:
q = new Queue(4), q.enqueue(8) -> q={8} (queue empty, B)
q = new Queue(4), q.enqueue(6), q.enqueue(5) -> q={6,5} (queue nonempty, C)

Test cases for method dequeue:
q = new Queue(0), q.dequeue() -> null, q={} (queue empty, A)
q = new Queue(3), q.dequeue() -> null, q={} (queue empty, B)
q = new Queue(3), q.enqueue(4), q.dequeue() -> 4, q={} (queue non-empty before call, C)
q = new Queue(1), q.enqueue(4), q.dequeue() -> 4, q={} (queue non-empty before call, D)
q = new Queue(3), q.enqueue(4), q.enqueue(6), q.dequeue() -> 4, q={6} (queue non-empty after, C)


  • Whenever you might have to test several things together, in designing tests you have a choice that must be driven by:
    • Traceability (from where did this defect came out?)
    • Readability (will any other programmer be able to read and understand the tests and their meaning in a reasonable amount of time?)
    among others. Bear also in mind that a test suite needs a proper design in the same way as a normal application does, so any time you write test code you should also keep an eye on how easy it will be to make it evolve together with the program it is testing.
  • A good practice is to keep the number of assertions per test case as low as possible to enforce that what is said in the previous bullet. The ideal is to have one assertion per test case. Although this leads to lots of test methods, this is the ideal. Every test case tests a certain property, so if one case fails you know exactly which property failed.
  • Scenarios in which multiple assertions are useful.
    • Logical expressions that are evaluated together. Imagine you have to assert that a&&b&&c is true. Then it makes sense to break
      since this will make any defect more traceable.
    • Strong semantic coupling between expressions. You can have situations in which the multiple assertions make sense together because they prove a property. An example it could be proving that two queues have the same values with the exception of the last one in one of them: you can then factor the two assertion in a single method.
            public void myAssertion(Queue a, Queue b){
      Obviously, assuming that dequeue is bug free and Queue implements equals.
  • Expected clauses. JUnit allows test-methods to fail with an exception, if it is explicitly is stated that this is expected to happen. So, if method m should throw a nullpointer exception if it gets the argument null as input, this can be tested with the test case:
    @Test(expected = NullPointerException.class)
    void testM() {

3 c) Derive test cases which have full statement coverage.

Statement coverage:

Test cases for constructor:
q = new Queue(3) -> q={} (only one path in constructor)

Test cases for method size:
q = new Queue(2), q.size() -> 0, q={} (only one path in method)

Test cases for method max:
q = new Queue(2), q.max() -> 2, q={} (only one path in method)

Test cases for method enqueue:
q = new Queue(1), q.enqueue(3) -> q={3} (the body of the if-statement is executed)

Test cases for method dequeue:
q = new Queue(3), q.dequeue() -> null, q={} (the body of the first if-statement is executed)
q = new Queue(1), q.enqueue(7), q.dequeue() -> 7, q={} (the rest of the statements are executed, including the body of the second if-statement)

3 d) Look at the specification you wrote so far and think about what they have in common.

There are some constraints on and relations among the values of the different instance variables which are contained in a queue. These are called invariants. You will see more in the rest of the course, but we can start thinking about that from now. The following properties have to hold in order to define precisely the instances of queues that implement the abstraction of a queue.

class invariant for Queue:
arr is non-null, and
0 <= size <= length of arr, and
0 <= first < length of arr, and
0 <= last < length of arr, and
either last - first = size or length of arr + last - first = size
The last line of the invariant has two cases in order to deal with the situations where the queue wraps around the beginning and end of the array.
It is interesting to see what happens if we keep invoking enqueue() on a certain queue:
q = new Queue(2) 	// size == 0, first == 0, last == 0 , q : [-,-]
q.enqueue(1); 		// size == 1, first == 0, last == 1 , q : [1,-]
q.enqueue(2); 		// size == 2, first == 0, last == 2 , q : [1,2]
q.enqueue(3);		// !! size == 3, first == 0, last == 0, q: [3,2]
In the third enqueue, the method ends normally: there is no exception. But we broke the invariant, and the abstraction we built on the array and the pointers: dequequing now will not give 1 as we expected.
An invariant is something the implementor has to assure that holds before and after the method has been executed. You could see it as a factoring out of things you would write in all the ensures and requires clauses of the specification. And, among the possible things that can happen after calling a method and not respecting its requirements, there can be even making false the invariant.
In exercise 2, try calling the method with two arrays of different lengths. Calling a method and not fulfilling the requires specification leads to an unpredictable behavior, not necessarily to the abrupt termination of your program.

Exercise 4

Consider this method:

  public static void f(Object x, Object[] arr) {
    int i;
    boolean exists = false;
    for (i = 0; i < arr.length; i++) {  // A1
      if (x.equals(arr[i])) {           // B1
        exists = true;
      }                                 // B2
    }                                   // A2
    if (!exists)                        // C1
      for (i = 0;; i++) {               // D1
        if (arr[i] == null) {           // E1
          arr[i] = x;
        }                               // E2
      }                                 // D2
    }                                   // C2

Someone wrote this specification for f:

specification for method f
  x and arr are non-null and there is an element in arr which is null
  when f returns there is an element in arr which is equal to x

4 a) The precondition (requires) can be made weaker. How?

If there is already an element in arr which is equal to x, then there need not be a null in arr. So the precondition can be:

x and arr are non-null and there is EITHER an element in arr which is null OR an element in arr which is equal to x
This means that either arr has some null elements, or the array has an element that is equal to x. But not both: i.e.
x = new Integer(1);
arr = new Integer[]{null,x};
violates the precondition.

4 b) The postconditions (ensures) can be made a bit stronger. How?

The elements which were previously in arr will still be there after the call. We can even say where x is inserted but let's keep the specification on a slightly more abstract level.

when f returns
  x is unchanged, and
  if there was before an object equal to x in arr then arr is unchanged,
  otherwise arr contains the same non-null objects plus x and the rest is unchanged

4 c) Derive test cases which together have full path coverage up to and including repeating for-loops twice.

Let's use these codes for referring to the different branch choices:

  • (A1) going into first for-loop
  • (A2) skipping/exiting first for-loop
  • (B1) going into if-statement in first for-loop
  • (B2) skipping it
  • (C1) going into if-statement after first for-loop
  • (C2) skipping it
  • (D1) going into second for-loop
  • (D2) skipping/exiting second for-loop
  • (E1) going into if-statement in second for-loop
  • (E2) skipping it
Path can be described as sequences of the codes above.

Test cases for path coverage up to two repetitions of for-loops:
arr = {null}, f(1, arr) -> arr={1} (A1,B2,A2,C1,D1,E1)
arr = {1}, f(1, arr) -> arr={1} (A1,B1,C2)
arr = {2,null}, f(1,arr) -> arr={2,1} (A1,B2,A1,B2,A2,C1,D1,E2,D1,E1)
arr = {null,2}, f(1,arr) -> arr={1,2} (A1,B2,A1,B2,A2,C1,D1,E1)
arr = {2,1}, f(1,arr) -> arr={2,1} (A1,B2,A1,B1,C2)

Exercise 5

We are going to specify and test an implementation of an algorithm called "Dutch National Flag". The algorithm can sort arrays arr of integers coming from the set {1,2,3} in linear time.

Example: Given the array

arr = {2,3,3,3,1,1,2,3,2,2,1,1,1}
the algorithm sorts the array, producing:
arr = {1,1,1,1,1,2,2,2,2,3,3,3,3}
When the array contains other numbers than 1, 2 or 3, the result is unpredictable.

Here is the code:

  public static void dnfsort(int[] arr) {
    int a = 0, b = 0, c = arr.length;
    while (b < c) {
      if (arr[b] == 1){
        arr[b] = arr[a];
        arr[a] = 1;
        a = a+1;
        b = b+1;
      } else {
        if (arr[b] == 2) {
          b = b+1;
        } else // arr[b] should be 3 here
          c = c-1;
          arr[b] = arr[c];
          arr[c] = 3;

5 a) What would be a suitable precondition of this code?

requires: arr is non null and all elements in arr are either 1,2 or 3

5 b) Here is a proposed postcondition of the code, expressing the sortedness of the result:

  when dnfsort returns then for all pairs of adjecent elements, say arr[i] and arr[i+1],
  it holds that arr[i] is less than or equal to arr[i+1].
What part of the behaviour of the algorithm does this postcondition not express?

It says that the result is a sorted array, but not that the array contains the same elements as before the call.

  when dfsort returns then for all pairs of adjecent elements, say arr[i] and arr[i+1],
  it holds that arr[i] is less than or equal to arr[i+1]
  and the elements in arr is a permutation of the elements in arr before the call

5 c) Using the precondition and postcondition you have now expressed, systematically derive test cases.

The array arr can can be either empty or non-empty. Thinking about how sortedness and permutation is defined, this also motivates dividing the test cases into 1-element arrays and several element arrays. Also the precondition enumerates the numbers 1,2 and 3, so different combinations of these numbers should form different classes.

arr = {}, dfsort(arr) -> arr={} (arr is empty)
arr = {1}, dfsort(arr) -> arr={1} (arr has length 1)
arr = {2}, dfsort(arr) -> arr={2} (arr has length 1)
arr = {3}, dfsort(arr) -> arr={3} (arr has length 1)
arr = {1,1}, dfsort(arr) -> arr={1,1} (arr has length > 1)
arr = {2,1}, dfsort(arr) -> arr={1,2} (arr has length > 1)
arr = {1,3}, dfsort(arr) -> arr={1,3} (arr has length > 1)
arr = {3,2}, dfsort(arr) -> arr={2,3} (arr has length > 1)
arr = {2,2}, dfsort(arr) -> arr={2,2} (arr has length > 1)

5 d) Looking at the code, construct a set of test cases such that full statement coverage is reached.

Statement coverage:
arr = {1}, dfsort(arr) -> arr={1} (first if then-part)
arr = {2}, dfsort(arr) -> arr={2} (first if else-part, second if then-part)
arr = {3}, dfsort(arr) -> arr={3} (first if else-part, second if else-part)

5 e) What are the branching points in the program? Construct a set of test cases such that full branching coverage is reached.

Branching points are the ifs and the while. The above test cases have also full branch coverage since the condition in the while loop will be both true and false for each example.

5 f) Give an example of a path through the program that is not covered by any of the above test cases.

Any path which repeats the while loop at least three times, e.g.:
arr = {1,3,2}, dfsort(arr) -> arr={1,2,3}

Home | Course | Schedule | Exam | Exercises | Labs | Evaluation | Tools | Links Atze van der Ploeg, Nov 4, 2015