OpenJML warning in Java

311 views Asked by At

I am new to JML warnings and I am trying to remove all warnings for this function:

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

But I am getting following errors:

 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;

Could someone help me figure out how to do this the correct way?

I updated to:

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

and now I am getting:

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

If I put this above, then I get an error the cannot find symbol i :(

0

There are 0 answers