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() {
}