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
:(