java - 关键 Java JML 证明程序通过了这个算法，该算法读取触发 NullPointerException 的特定数组元素？它应该失败

Question

我很想更好地理解 Java 密钥证明的限制。我想出了一个特定的数组元素将触发空指针异常的场景。当我通过证明程序运行它时，它通过了。知道这是为什么吗？它应该会失败，因为将在数组元素 86454 处抛出空指针。请注意“normal_behaviour”意味着它应该无异常终止。

/*@ 
 @ 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;
}

Answer 1

您的规范仅涵盖正常行为，而不是例外情况。

正常行为意味着，在方法执行之后，必须遵守所有后置条件。因此，存在一个返回值，您可以访问它（\result）。对于特殊情况，您的requires子句定义不明确。

如果要指定情况，则应在发生异常时使用exceptional_behavior，并且在要显示“无异常”的情况下使用behavior。两者都与signals从句连用。例如，使用以下内容来显示无异常性：

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

此合同不能由可能引发异常的方法来履行。

请参考关键书的第7章（尤其是“7.3.3 正常行为规范案例的语义”）。