2D1455 - 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.

  1. 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.

  2. 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.)

  3. 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?

  4. 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?

  5. 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 second-order logical language. Could you express these two requirements in that language, and if so what does that say about JML and weak second-order 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!