Compact constructors and JML

[wadoon]

Considering the following example of a simple Record with a compact constructor:

public record Point2dU(int x, int y) {
    Point2dU {
        if(x<0) x *= -1;
        if(y<0) y *= -1;
    }
}

by conversion it is similar to

public class Point2dU {
    private final int x; private final int y;
    public Point2dU((int x, int y) {
        if(x<0) x *= -1;
        if(y<0) y *= -1;
        this.x = x; this.y = y;
    }
    ...
}

Now, the constructor behavior is modified by the compact constructor code.

How can I describe the synthetic constructor behavior?

The recent version of JmlRef does not cover this.

Questions

Where should the contract be?

1. On the record

   /*@ ensures this.x>0 && this.y>0; */
   record Point2d(int x, int y) { ... } 
   

2. On the compact constructor

   record Point2d(int x, int y) { 
      /*@ ensures this.x>0 && this.y>0; */
      Point2d { ... } 
   } 
   

When a contract is given, should the synthetic contract (e.g., ensures this.x == x ...;) still be injected?

[davidcok]

The documentation in the refman is not yet up to date with the implementation.

The contract should be applied to the constructor, compact or not. There may well be more than one constructor.

Here is example working specs:

public record Point2dU(int x, int y) {
    //@ requires x > Integer.MIN_VALUE;
    //@ requires y > Integer.MIN_VALUE;
    //@ ensures \old(x) >= 0 ==> this.x == x;
    //@ ensures \old(x) <  0 ==> this.x == -x;
    public Point2dU {
        if(x<0) x *= -1;
        if(y<0) y *= -1;
    }
}

or

public class Point2dU {
    /*@ spec_public */ private final int x; /*@ spec_public */ private final int y;
    //@ requires x > Integer.MIN_VALUE;
    //@ requires y > Integer.MIN_VALUE;
    //@ ensures \old(x) >= 0 ==> this.x == \old(x);
    //@ ensures \old(x) <  0 ==> this.x == -\old(x);
    public Point2dU(int x, int y) {
        if(x<0) x *= -1;
        if(y<0) y *= -1;
        this.x = x; this.y = y;
    }
}