You can download the Java sources for the exercises here.

You can download the solutions for the exercises here.

Exercise 1

What does the following method do, assuming that x is non-negative?

public int x;

public int method() {
  int y = x;
  int z = 0;

  while (y > 0) {
    z = z + x;
    y = y - 1;
  }

 return z;
}

1. Write JML specifications for method and invariants for the class (see loops/ex1).
2. Prove partial correctness for method by providing a loop invariant.
3. Is total correctness possible to prove? Justify!

Exercise 2

What does the following method do, assuming that x is non-negative and y is positive?

public int x;
public int y;

public int method() {
  int x1 = x, q = 0;

  while (x1 >= y) {
    x1 = x1 - y;
    q = q + 1;
  }

 return q;
}

1. Write JML specifications for method and invariants for the class (see loops/ex2).
2. Prove partial correctness for method by providing a loop invariant.
3. Is total correctness possible to prove? Justify!

Exercise 3

What does the following method do?

public int a[];

public void method() {
  for (int i = 0; i < a.length; i++) {
    if (a[i] < 0)
      a[i] *= -1;
  }
}

1. Write JML specifications for method and invariants for the class (see loops/ex3).
2. Prove partial correctness for method by providing a loop invariant.
3. Is total correctness possible to prove? Justify!

Exercise 4

Verify that method replaceIfGreater of class ArrayHelper in directory verify/ex4 ensures its postconditions. Explain how you can read from the open goal(s) and the path to an open goal, what is going on. Fix then the bug in the specification or implementation and verify the method again.

Exercise 5

The directory verify/ex5 contains a few classes. One of them is the class Person. Imagine the class belongs to a database of the authority responsible for issuing driver licenses. Further each person in this database has already successfully passed all tests. So each person has already a driver license, but some are still not old enough to actually be allowed to drive. You need to have fulfilled your 18th year to get the allowance. The allowance is issued by activating the license of a person.

1. Specify the normal and exceptional behavior of method activateLicense of class Person.
2. Verify that both contracts ensure their respective postcondition.
3. Verify that the method activateLicense preserves the invariants of class Person.

If one of the above proofs cannot be closed, try to find out why by looking at the proof. To which actual situation(s) do the open goals belong? What kind of hints can you read from the sequent of an open goal?

Exercise 6

Consider the class Hashtable in verify/ex6. This class represents an open addressing hash table with linear probing as collision resolution. Within a hash table, objects are stored into a fixed array h. Besides, in order to have an easy way of checking whether or not the capacity of h is reached (i.e. the array h is full), a field size keeps track of the number of stored objects and a field capacity represents the total amount of objects that can be added to the hash table.

The method add, which is used to add objects to the hash table, first tries to put the corresponding object at the position of the computed hash code. However, if that index is occupied, then add searches upwards (modulo the array length) for the nearest following index which is free. A position is considered free if and only if it contains a null object.

Augment class Hashtable with JML annotations stating the following:

• The size field is never negative, and always less or equal than capacity.
• The capacity should be the same value as h.length.
• The array h cannot be null.
• There should be space for at least one element in the hash table.
• The number of elements stored in array h (i.e., the number of array cells whose content is not null) is size.
• If the size is strictly smaller than capacity, then all of the following must hold:
  • add terminates normally
  • add increases size by one
  • After add(obj,key), the object obj is stored in h at some index i.

In addition:

• Write assignable clauses where appropriate.
• Write class invariants.
• Write a loop invariant, decreases clause, and assignable clause for the loop in method add.
• Add JML modifiers where necessary.

Exercise 7

On this exercise we will analyse the specification and implentation of the class Coordinate in verify/ex7, which represents the coordinates of a cartesian coordinate system. When checking the content of this class, you will notice the presence of several erroneous situations, e.g. a method not fulfilling its specification (i.e. moveRight), a nonsense specification (i.e. explotion method specification), etc.

Now that you are aware of these issues, do you think that it is possible to prove that the method translation fulfills its specification? Justify!