– title: JML Tutorial - Exercises - Answers to Postcondition Exercises –

Postconditions Exercises

Question 1

(a) The method would fail to verify with the new precondition because when the value of num is zero, then the value returned (num*2) would not be strictly greater than num, as it would also be zero.

To check this, observe ESC’s output for this code is as follows. The second error message, which says that OpenJML cannot verify the postcondition is failing happends precisely because num may be 0. You can check this by adding a show statement before the return statement in the body, which will show that the counterexample is happening when num is 0.

PostCondEx1a.java:7: verify: The prover cannot establish an assertion (Postcondition: PostCondEx1a.java:5:) in method multiplyByTwo
        return num*2;    // ERROR: may not satisfy postcondition!
        ^
PostCondEx1a.java:5: verify: Associated declaration: PostCondEx1a.java:7:
    //@ ensures num < \result;
        ^
2 verification failures

(b) A simple fix to the postcondition is to change < to <=, which will allow the method to return 0 when the argument is 0. This directly addresses the problem noted above. Thus the code below verifies.

    //@ requires -1 < num < 100;
    //@ ensures num <= \result;
    public int multiplyByTwo(int num) {
	return num*2;
    }

Question 2

A postcondition that can be used to make the code verify is \result == num / 2. (Any equivalent expression will do, including 2*\result == num, but the theorem provers, SMT solvers, used in OpenJML cannot reason about multiplication and division, so OpenJML may still complain.)

Question 3

The answer to this question depends on the code you write. However, if you write the obvious body

    return w*h;

Then it is necessary to prevent integer overflow, so a suitable precondition could be

   w*h <= Integer.MAX_VALUE

which could be put in a requires clause. A suitable postcondition for this would be

   \result == w*h

which could be put in an ensures clause.

Thus an entire solution could look like the following.

// openjml --esc Rectangle.java
public class Rectangle {

    //@ requires 0 < w;
    //@ requires 0 < h;
    //@ requires w*h <= Integer.MAX_VALUE;
    //@ ensures \result == w*h;
    public int area(int w, int h) {
        return w*h;
    }
    
}

Question 4

The answer can vary, but one possible specification and implementation is the following.

    /*@ requires !Double.isNaN(x);
      @ requires !Double.isNaN(y);
      @ ensures Math.abs(\result - (x+y)/2.0) < 0.001; @*/
    public double average(double x, double y) {
        return (x+y)/2.0;
    }

(Currently, in OpenJML 21.0.28, the requires clauses are not needed for the above to verify, but if one of the arguments is NaN, then the postcondition should be false. So it is always good practice to rule out NaN, as otherwise the implementation cannot be correct.)

Notice that the specification above only requires that the result be approximately equal to the expected value, although the approximation might vary. Since floating point arithmetic is only an approximation of real arithmetic, it is best to never compare floating point numbers for equality using == (or !=).