Here are some solution notes for the exercises in week 2. 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 to 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.

1a
What does this method do?

  specification for method reverse
  requires: nothing
  ensures:  a is unchanged
            and
            returns 
              null if a is null,
              otherwise an array in which 
                for all elements at index i it is equal (even identical) to a[n-1-i] where n is the length of a

  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;
  }

Notes

• Types don't change, therefore there is no need to enforce in the specification that what you have remains of the same type


• Length of the array does not change after the method returns, i.e. it has not to be affirmed in the postcondition. In the case of Java, any attempt to assign any other value to the formal parameters of the method will not be reflected in any changes to 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 is the content of the array, but not the array itself. (The same applies to any object.)


• The specification can also be divided in two different contracts:

specification for method reverse, first contract
requires: a is null
ensures:  returns null
  

and

specification for method reverse, second contract
requires: a is not null
ensures:  a is unchanged
	returns an array in which for all elements at index i it is equal (even identical) to a[n-1-i] where n is the length of a
  

Both, put in disjunction, form the specification for the method.

1b
(White-box testing) Derive test cases which together have full statement coverage. Then add test cases if necessary to have full branch coverage. Statement coverage:
reverse(null) -> null (executes the then-part of the if statement)
reverse({1}) -> {1} (executes the rest of the method, including the body of the for-loop

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

• A test suite fulfilling statement coverage on a code that branches with if/else (like the one here) achieves automatically branch coverage. Statement coverage can be fulfilled without fulfilling branch coverage if you have programs like

    ...
    if(condition){
      <statements_1>
    }
    <statements_2>
    ...
  

  which can be covered by a test case in which condition evaluates to true. So the absence of such a morphology allows you to obtain statement and branch coverage at once. A similar argument on program structure can be done with branch to path coverage, where there are multiple ifs.

    ...
    if(a){
      <statements_1>
    }
    if(b){
      <statements_2>	
    }
    
    ...
  

  In the above example, testing with (a=true,b=false), (a=true,b=false), (a=false, b=true) fulfills branch coverage but not path coverage (the suite lacks the case (a=true,b=true) which is an uncovered path).
  The same applies to programs with any looping that are known to unfold a fixed number of times -- think about for instance reading data from an 8 bytes buffer:

    for(i = 0; i<8; i++){
      <read one byte>	
    }
  

  These constructs presented so far are the cause of the differences between the presented criteria. In all the cases above you can find a test suite that fulfills criterion A but not any stronger criterion B (among the ones we seen so far.) A bigger jump is done when unbounded loops are allowed in the code, which makes path coverage impossible to achieve.

2a
What does this method do?

  specification for method vector_add
  requires: 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.
  ensures:  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
	

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

Notes:

• 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.
• A specification is a contract, i.e. an agreement between client and implementor. When the two parts accept the contract, they both have to accept and respect their duties to honour the contract. A client then, in order to have what it's written in the postcondition, must fulfill the precondition. Dually, the implementor, when a client satisfies the precondition, has to provide the postcondition.

2b
(Black-box testing) Derive test cases for the method.
The specification does not contain any case distinctions. The only thing to use is the presence of arrays a and b. We can distinguish between empty and non-empty arrays. This is what is called an implicit disjunction. The precondition rules out the cases in which the arguments have different lengths; therefore we can partition the input between a couple of zero length arrays, and a couple of non-zero length arrays (without null elements).
a={},b={},vector_add(a,b) -> a={},b={} (a and b have length 0)
a={5.5},b={3.2},vector_add(a,b) -> a={8.5},b={3.2} (a and b have length greater than 0)

3
This exercise was rather hard as it introduced some other things you will see later in the course. You should check carefully the implementation of the queue, as it is necessary to understand how things work.

3a
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 implementors of this specification to use different implementations, but then they have to define the mapping between how the instance changes with respect of the model.

public class Queue {
  Object[] arr;
  int size;
  int first;
  int last;
specification for constructor Queue
requires: max >= 0
ensures: a state representing an empty queue (size = 0)

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

specification for method size
requires: nothing
ensures: returns the value of the size attribute and the state of the instance is unchanged

  public int size() {
    return size;
  }
specification for method max
requires: nothing
ensures: the maximum capacity of the queue

  public int max() {
    return arr.length;
  }

specification for method enqueue
requires: size < length of arr
ensures: x is added to the queue (size increases by one)

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

specification for method dequeue
requires: nothing
ensures: 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

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

3b
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

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)

Notes.

• Here you can find a proposed way on how to translate the above tests in JUnit format. The proposed implementation uses the TestSuite class and inheritance. There is one class for each method to test.


• 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. Keep also in mind that a test suite needs a proper design in the same way as a normal application does, so anytime 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 what said in the previous bullet. Anyway there might be (and there will be) situations you might deviate from this. The ideal is to have one assertion per test case. This leads to lots of test methods, even though is the ideal (every test case tests a certain property).


• Scenarios in which multiple assertions are deleterious. JUnit, whenever an assertion fails, throws an exception that causes the abrupt termination of the test case. Therefore, in general, you might not have the entire picture of the defects your program has. This is mainly due to the ordering in which you put your assertions. Consider the following situation:

  Assert.assertEquals(a[4],c);
  Assert.assertEquals(a.length, s);
  

  Imagine a situation in which both would fail (e.g. if s==2), and the fact that the second one fails could be one cause of the failure of the first one. Then you will have to go and trace back the problem when you could have had more hints from the outcome of the test, if it was better engineered.
  


• 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

    assert(a&&b&&c);
    

    in

    assert(a);
    assert(b);
    assert(c);
    

    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){
      assertEquals(a.size,b.size);
      a.dequeue();
      assertEquals(a,b);
    }
    

    Obviously, assuming that dequeue is bug free and Queue implements equals.
  
  
• Soft assertions and multiple assertions. In Java you can always catch the exception and let the test continue. However, in the Assert package there is no such possibility. The underlying philosophy is that if there is a failure, then it does not matter going on with the test because you have to solve that problem first, or: if there has been a failure, how much can you trust a passed or failed assertion? ANYWAY, there are cases where multiple assertions'outcomes are useful because you know that you can trust their outcomes. In this case you can define for instance the SoftAssert class:

  
  public class SoftAssert{
  
    private StringBuffer strbf = new StringBuffer();
    private boolean passed = true;
    
    public void softAssertEquals(int expected, int actual, String m){
      try{
        Assert.assertEquals(expected,actual,m);
      }catch(AssertionError ae){
        passed = false;
        strbf.append(ae.getMessage());
        strbf.append("\n");
      }
    }
    
    public void hasPassed(){
      return passed;
    }
  }
  

  Then for instance in the previous example you would write

    SoftAssert sa = new SoftAssert();
    sa.softAssertEquals(a[4],c,"Position 4 does not contain "+c);
    sa.softAssertEquals(array.length, s,"Size is not "+s);  
    Assert.assertTrue(sa.hasPassed());
  

  so that if there were soft assertions violated, you will have it reported. NOTE HOWEVER that it is crucial to engineer properly your tests. A test should test only one thing, in the same way as a method in your program does only one thing (principle of single responsibility). Note also that in the case of the myAssertion example above, the soft assertion solution does not work properly because you change the state from an infected state.

3c
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)


---

Remarks:
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 to 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.

---

4
Consider this method:

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

  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;
        break;
      }                               // B2
    }                                 // A2
    if (!exists)                      // C1
    {
      for (i = 0;; i++) {             // D1
        if (arr[i] == null) {         // E1
          arr[i] = x;
          break;
        }                             // E2
      }                               // D2
    }                                 // C2
  }

4a
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};
f(x,arr)

violates the precondition.

4b
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

4c
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)


---

  public static void dfsort(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
We are going to specify and test an implementation of an algorithm called "Dutch 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.

5a
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

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

ensures: when dfsort return 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.

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

5c
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 = {1,2}, dfsort(arr) -> arr={1,2} (arr has length > 1)
arr = {1,3}, dfsort(arr) -> arr={1,3} (arr has length > 1)
arr = {2,1}, dfsort(arr) -> arr={2,1} (arr has length > 1)
arr = {2,2}, dfsort(arr) -> arr={2,2} (arr has length > 1)
etc

5d
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)


5e
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.

5f
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}