2

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

user122222
  • 2,179
  • 4
  • 35
  • 78
  • 1
    The loop invariant does not hold. The preconditions allow `input == 1` and the first two ifs at the start of the method are not satisfied with this. Execution therefore reaches the loop. There, `var i = input - 1` gets initialized to `i == 0`, violating the second part of the loop invariant `... && i > 1`. I think you want `i > 0`. – Michel K May 08 '22 at 17:17
  • 1
    The ` ArithmeticOperationRange` problem is reported because there can be an overflow. The preconditions allow `input == Integer.MAX_VALUE`, but even small factorials like `100!` are huge (ca. 9.3e157) and far greater than `Long.MAX_VALUE`. – Michel K May 08 '22 at 17:25
  • @MichelK thanks! updated my question. Could you please see if you can comment on that one too? – user122222 May 08 '22 at 18:26
  • 1
    I'm not familiar with OpenJML, but isn't `ensure` for method contracts (and not for statements)? Try `assert` instead, but I don't think that `\old` can be used in that case. Consider leaving that line away because it's literally the same as the code. – Michel K May 08 '22 at 19:40
  • `//@ ensures result == \old(result) * i;` is wrong. You want to put this condition into the loop invariant. OpenJML expects a refining statement, which allows to add a contract add on statements. Similar to block contracts in KeY. Also, you should revise your pre-condition: `//@ requires \forall long i; i == - 1; i > 0;` is `false`. – wadoon May 09 '22 at 21:30

0 Answers0