java - JML - 具有扩展静态检查的 OpenJML - 数组示例

Question

我刚开始使用 OpenJML，这里是我的代码和我的 JML 警告：

代码 ：

//@ requires myArray != null ;
//@ ensures myArray == \old(myArray) ;
//@ signals ( MathLibException ) myArray.size() == 1 ;
public ArrayList<Integer> ExceptionTest1 (ArrayList<Integer> myArray) throws MathLibException
{
    if ( myArray.size() == 1  )
    {
        throw new MathLibException();
    }
    else
        return arraylist;
}

JML 警告：

我不明白为什么无法建立特殊的后置条件。

谢谢您的帮助

Answer 1

问题解决，

我的异常并不纯粹，使用此代码，它可以正常工作：

    public /*@ pure @*/ MathLibException() {
}