Formal specification and verification using JML

Formal specification and verification using JML

     [http://www.cs.ru.nl/~erikpoll/Teaching/CSIS/opdracht.html]

Hand in exercise 1 & 2 & 3 - ie. your cumulative result after exercise 3 - by email to Richard, unless this was signed off on Thursday afternoon already. Provide your answer as a single attachment entitled TaxpayerYOURFULLNAME.java, and don't zip, tar, ... it.

Goal of this exercise are to experience

The formal specification language we use is JML, which allows us to express contraints in propositional and predicate logic about Java programs. The tool we use is the verification tool ESC/Java2, which is an automated program verification tool for Java programs.

Running ESC/Java2

ESC/Java2 is available on the central UNIX machines (e.g. solost) and on the Windows PCs in the terminal rooms. You can also download it on your own machine. Instructions for this:

The assignment, part 1

For the assignment, download the file Taxpayer.java. This class is used in an information system at the tax office to record information about persons. The tax office want to ensure that the following properties hold:
  1. Persons are either male or female.
  2. Persons can marry to people of the opposite sex. (A bit outdated maybe, but makes for interesting properties to specify).
  3. A very obvious constraint, but easy to overlook: if person x is married to person y, then person should of course also be married, and to person x.
Your assignment is to
  1. add invariants to the code below to express the constraints mentioned above, in JML syntax, plus any other sensible constraints you can think of;
  2. use ESC/Java2 to detect possible violations, which are reported as warnings
  3. for the Java methods that ESC/Java2 complains about fix this, by
    1. correcting the code, or
    2. adding a (sensible) precondition for the method, using a JML requires clause, or
    3. sometimes, adding an invariant to record another constraint can help in verification.
Hints In the end, ESC/Java2 should run without any complaints on the annotated code, meaning that it has succeeded in verifying that the code meets the formal specification.

JML syntax

Below the syntax for Java and JML logical connectives, in order of decreasing precedence:

logical connective    Java/JML syntax
not !
equality ==
inquality !=
conjunction (and) &&
disjunction (or) ||
implication ==> , <==
(in)equivalence <==> , <=!=>
In addition to this, you can use standard Java syntax, so you can say things such as 

  this.spouse != null ==> (this.spouse.spouse.isFemale ==> this.isFemale)
Of course, you can write spouse instead of this.spouse, leaving this implicit. Note that in Java, as in most programming languages, references such as the spouse field, can be null. Often fields should not be null under certain circumstances, which can be expressed by an invariant of the form 
 //@ invariant  .... ==> spouse !=null;
Often arguments of method should not be null, which can be expressed by a precondition of the form 
 //@ requires new_spouse != null;
 void marry (Taxpayer new_spouse) {

The assignment, part 2

The tax system uses a income tax allowance (belastingvrije voet):
  1. Every person has an income tax allowance, over which means they do not have to pay tax over the first part of their income. There is a default tax allowance of 5000.
  2. Married persons can pool their tax allowance, as long as the sum of their tax allowances remains the same. For example, the wife could have a tax allowance of 10000, and the husband a tax allowance of 0.
Add invariants that express these constraints, and if necessary fix/improve the code to ensure that they are not violated.

The assignment, part 3

The new government introduces a measure that people aged 65 and over have a higher tax allowance, of 7000. The rules for pooling tax allowances remain the same.

Add invariants that express these constraints, and if necessary fix/improve the code to ensure that they are not violated.

The assignment, part 4

WARNING: things may get a bit hairy here, so don't be too depressed if you don't manage to finish this.

The minister for Jeugd en Gezin, André Rouvoet, introduces a new tax measure giving anyone with underage children an additional tax allowance of 1000 euro.

The taxpayer class is extended with an additional field to keep track of the youngest child 

   Taxpayer youngestChild;    // youngest child of this person
and the two following lines are added to the constructor 
   Taxpayer(boolean jongetje, Taxpayer ma, Taxpayer pa) {
      ...
      youngestChild = null;           // NEW
      ma.youngestChild = this;    // NEW
      pa.youngestChild = this;    // NEW
   }

Add the three lines above to your code, add invariant(s) to express the new government policy above, and re-run ESC/Java2 and fix the code to ensure that it is not violated.

General hints

Some hints to keep you out of trouble with the tool:

Reflection

Some questions to consider
  1. In the end, do you think that you found all problems? Are you certain now that the code is correct?
  2. Can you think of ways in which the tool or the specification language could be improved?
  3. Can you think of other situations where a similar kind of tool support could be useful?
  4. Instead of the tool we used, can you think of other ways (formal or informal, tool-supported or not) to find the problems that the tool found? If so, would these alternatives