DD2456  Laboratory Exercise 4.
Formal Verification with ESC Java.
In this lab you will have the chance to
experiment with writing formal assertions for Java programs using the
Java Modeling Language (JML). You can then check whether your formal assertions are true
or false by using the Extended Static Checker for Java (Version 2, ESC/Java2).
Although you will only be using a small subset of what JML can express, you will
quickly encounter what appear to be limitations in the language. You may compare
the design of JML with the weak second order language encountered in lectures, which is
known to be a complete language and logic.
1. Getting Started
If you do not have access to ESC/Java2 on your machine you can find
download and installation details here.
I suggest you consider using a Unix terminal, but you should be able to run the tool
anywhere, including on a PC or Mac at home, as it is written in Java. Note it *only* runs on the Java 1.4 vm and *not* the 1.5 vm, so you may have to set up a script to set up variables and values
that will allow you to use 1.4.
To get started and get the feel of the program, I suggest you write a small
Java program e.g. Myaddition.java, which uses the simple while program described in the
lecture notes to add two integers. Write a method such as myaddition(int x, int y),
and add the pre and postconditions discussed in class.
You can verify this simple example by typing:
escjava2 Myaddition.java
By adding any necessary invariants discussed in class, get ESC/Java2 to verify this simple
algorithm. What is the smallest number of invariants that still lead to an automatic verification?
Try changing the int types to Integer object types in your code. Do you observe any new
error messages? What preconditions must be added to remove these?
1.1. The Main Exercise
After some basic experimentation with the system (you can continue by
considering other examples discussed in class if you wish) you are ready
to proceed with the main lab exercise as follows.
Your main task is to formally verify a sorting algorithm of your choice.
 Begin by formally specifying in JML what it means to sort an array of integers, either
into linearly ascending or descending order. Notice that this specification
is general and should be correct for *any* sorting algorithm you choose.

There are many sorting algorithms known, such as insertion sort, heapsort, mergesort, etc.
Choose one of them and encode it as a Java method in such a way that your specification for
part (1) can be applied to it (i.e. the method has the right interface.)
 Now using ESC/Java2 and any invariant assertions which may be necessary,
make a formal verification of your encoding of your sorting algorithm.
What is the smallest number of assertions that you need to add to the code
to get the verification to go through, and where do you need to add them?

Introduce some deliberate errors into your code (if there were none to begin with) and
observe what error messages you obtain. Do you always obtain an error message?
Is it always appropriate or correct?

You can now test the limits of JMLs expressiveness in the following way.
To sort an array of integers, it is not sufficient that the output is linearly
ordered. It must satisfy two extra conditions:
(i) every output array element comes
from some input array element, i.e. the sorting algorithm does
not *add* anything to the input array, and,
(ii) every input array element
appears as some output array element, i.e. the sorting algorithm does not
*delete* anything from the input array.
In other words, the ouput array must be a permutation of the input array.
Your task is to try to model these two extra requirements in JML as accurately as you can.
Is it enough to talk about the lengths of the input and output arrays, or does this
still leave open possibilities for errors?
On thinking seriously about this issue, you may wonder if a *perfect* answer can be expressed
in JML at all! Compare JML with our complete weak secondorder logical language.
Could you express these two requirements in that language, and if so what does
that say about JML and weak secondorder logic?
.
1.2. To hand in
For both parts of the lab exercise (i.e. the simple sorting specification and the
advanced sorting specification)
you should hand in your Java code for your sorting algorithm of choice, together
with a transcript of the output from your final ESC/Java2 run.
If your code is not sufficiently precise or ESC/Java2 gives warnings or errors
that I judge should not occur I will give you a critique and ask you to complete the
assignment. Otherwise you will pass the lab exercise.
There is no deadline for this lab, but be aware of the deadlines
for LADOK points. Please do not wait until the last week of term and expect
that I will have time to mark your work immediately then!