Expecting PreconditionError but got NullPointerException

Question

I have a class Natural with a precondition before the constructor method (notice the requires).

public class Natural {
private int data;

@Requires("n != null")
public Natural(Natural n) {
    this(n.data);
 }
}

This is the test for that Precondition. It tests the constructor for a null input.

@Test(expected = PreconditionError.class)
public void testConstructorWrong2() {
    Natural n = new Natural(null);
}

The test should pass, because this test expects a violation of the Precondition. But I am getting NullPonterException instead.

Answer 1

As stated on the Cofoja page:

However, a very important distinction is that constructor preconditions are checked after any call to a parent constructor. This is due to super calls being necessarily the first instruction of any constructor call, making it impossible to insert precondition checks before them. (This is considered a known bug.

The above probably applies to this as well as super. The @Requires condition can only be checked after the call to this(n.data); because Java won't allow anything to come before it. And so, the call to n.data throws a NullPointerException before the annotation even has a chance to check the precondition.

If you still want to check the precondition, you will have to remove the call to this(...) and initialize the object directly

@Requires("n != null")
public Natural(Natural n) {
  this.data = n.data;
}