Предупреждение OpenJML в Java

Question

Я новичок в предупреждениях JML и пытаюсь удалить все предупреждения для этой функции:

      //@ requires input <= Integer.MAX_VALUE;
//@ requires input >= 0;
//@ ensures \result >= 0;
//@ signals (Exception) input >= Integer.MAX_VALUE;
//@ ensures result == \old(result) * i;
public /*@ pure @*/ long calculateFactorial(int input) throws Exception {
    int result = 1;
    if (input <= 0) {
        return result;
    }
    else if (input >= Integer.MAX_VALUE) {
       throw new Exception();
    }
    result = input;

    //@ loop_invariant i < input && i > 1;
    for (var i = input - 1; i > 1; i--) {
        result = result * i;
    }
    return result;
}

Но я получаю следующие ошибки:

       The prover cannot establish an assertion (LoopInvariantBeforeLoop) in method calculateFactorial
 //@ loop_invariant i < input && i > 1;
        ^
MathProblems.java:29: verify: The prover cannot establish an assertion 
(LoopInvariant) in method calculateFactorial
    //@ loop_invariant i < input && i > 1;
        ^
MathProblems.java:31: verify: The prover cannot establish an assertion 
(ArithmeticOperationRange) in method calculateFactorial: int multiply overflow
        result = result * i;

Может ли кто-нибудь помочь мне понять, как это сделать правильно?

Я обновился до:

      //@ requires input < 21;
//@ requires input >= 0;
//@ requires \forall long i; i == - 1; i > 0;
//@ ensures \result >= 0;
//@ signals (Exception) input > 20;
public /*@ pure @*/ long calculateFactorial(long input) throws Exception {
    long result = 1;
    if (input <= 0) {
        return result;
    }
    else if (input > 20) {
       throw new Exception();
    }
    result = input;

    //@ loop_invariant i < input && i > 0;
    //@ loop_decreases i - 1;
    for (long i = input - 1; i > 1; i--) {
        //@ ensures result == \old(result) * i;
        result = result * i;
    }
    return result;
}

и теперь я получаю:

       warning: A refining statement is required for statement specifications
        //@ ensures result == \old(result) * i;

Если я поставлю это выше, то я получаю сообщение об ошибке, не могу найти символ i:(