0

I'm tyring to better understand the limits of the Key proover for Java. I have come up with a scenario where a specific array element will trigger a null pointer exception. When I run this through the proover it passes. Any idea why this is? It should fail as the null pointer will be thrown at array element 86454. Please note "normal_behaviour" means that it should terminate without exceptions.

/*@ 
 @ normal_behaviour
 @ requires true;
 @ ensures \result == 7;
 @*/ 
public static int tmp() {
    Object[] arr = new Object[999999];
    arr[86454] = new Integer(6);
    for (int i=0;i<999999;i++){
        if (arr[i]!=null && arr[i].equals(new Integer(6))){
            throw new NullPointerException();
        }
    }
    return 7;
}
newlogic
  • 807
  • 8
  • 25

1 Answers1

0

Your specification only covers the normal behaviour, and not the exceptional case.

Normal behaviour means, that all post-condition have to be adhered, after the method is executed. Therefore, there exists a return value, and you are allowed to access it (\result). For the exceptional case, your requires clause would not be well-defined.

If you want to the specify the case, when an exception occurs you should use exceptional_behavior and in the case you want to show the "exception-freeness" use behavior. Both in conjunction with a signals clause. For example, use the following to show the exception-freeness:

/*@ public behavior 
    requires true; 
    signals (Exception e) false;
*/

This contract can not fulfilled by a method, which could throw an exception.

Please refer to Chapter 7 (especially "7.3.3 Semantics of Normal Behavior Specification Cases") of the key book.

wadoon
  • 51
  • 3
  • The normal_behaviour clause does not allow any exceptions as default. "The normal behavior gets an additional clause signals (Throwable t) false" 8.2 of the Key Deductive Software Verification book (2016). I don't see how this method can be passed by the verifier, it will always throw a NullPointerException. Requires has no effect as its set to true and therefore any pre state is allowed. – newlogic Jul 15 '20 at 11:41