Taxpayer exercise

Part 1

1. Persons are either male or female.
2. Persons can only marry to people of the opposite sex. (A bit outdated maybe, but makes for interesting properties to specify).
3. A very obvious property, but easy to overlook: if person x is married to person y, then person should of course also be married, and to person x.

1. add invariants to the code below to express the properties mentioned above, in JML syntax, plus any other sensible properties 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 property can help in verification.

• Only look at the first warning that ESC/Java2 produces, and ignore the others, until you've managed to get rid of this first one.
• The code of the methods marry and divorce in the class Taxpayer is not correct. ESC/Java2 should detect this and complain about these methods once you've added your invariants, and you will have to add a few lines of code to fix these methods, and possibly also add a precondition by means of a requires clause.
• It is easiest to introduce one invariant at a time, then fix the errors this brings to light, and only then move on to the next one.
• If the tool produces some warnings, ie. if the tool thinks that some property is not satisfied by the code, this can have several causes:
  • There is an error in the code, which results in a violation in the Java code. For example, an assignment to some field may be missing.
  • There is an error in the JML specification. For example, maybe you have written "and" in a specifcation where you meant "or", maybe you have written age > 18 when you meant age >= 18 in some constraint
  • There may be some properties missing, which are needed by the tool for the verification. Note that the tool does not know any of the things that may be obvious to you -- for example, that if some person x is married to y then y is also married to x -- and such properties may be needed for verification.
  • In general, a warning might be caused by the fact that some property is too difficult for the theorem prover to proof: an automated theorem prover can only ever prove properties of a certain, limited complexity. However, for the exercises here you should not run into this problem.
  To stop the tool from complaining, you can
  • correct the Java program; for the exercise here this should only involve adding some simple assignments to the offending method;
  • correct the JML specification;
  • specify some additional properties, either as a JML invariant or as JML precondition aka requires clause.

JML syntax

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)

 //@ invariant  .... ==> spouse !=null;

 //@ requires new_spouse != null;
 void marry (Taxpayer new_spouse) {

Part 2

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.

Part 3

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

Part 4

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

   Taxpayer(boolean jongetje, Taxpayer mum, Taxpayer dad) {
      ...
      youngestChild = null;        // NEW
      mum.youngestChild = this;    // NEW
      dad.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

• Don't use method invocations inside methods for this exercise.
• Don't use the Java shorthand x+=10 for x = x+10.
• Whenever possible, split invariants than contain conjunctions into several smaller invariants. This improves feedback of the tool. So instead of
     //@ invariant A && B;
  write
     //@ invariant A;
     //@ invariant B;>
  The same goes for preconditions (aka requires clauses).
• If the tool complains of invariant violations, it produces a lot of feedback that is hard to interpret. The crucial information to look at is
  • the line number saying which invariant is violated, and
  • the line number saying where this invariant is violated.
  NB beware that calling a method may break on some object may break the invariant of another object; for instance, in the taxpayer exercise, calling a method on a TaxPayer may break the invariant of his or her spouse.