title: OpenJML warning in Java
body: <p>I am new to JML warnings and I am trying to remove all warnings for this function:</p>
  <pre><code>//@ requires input &lt;= Integer.MAX_VALUE;
  //@ requires input &gt;= 0;
  //@ ensures \result &gt;= 0;
  //@ signals (Exception) input &gt;= Integer.MAX_VALUE;
  //@ ensures result == \old(result) * i;
  public /*@ pure @*/ long calculateFactorial(int input) throws Exception {
      int result = 1;
      if (input &lt;= 0) {
          return result;
      }
      else if (input &gt;= Integer.MAX_VALUE) {
         throw new Exception();
      }
      result = input;
  
      //@ loop_invariant i &lt; input &amp;&amp; i &gt; 1;
      for (var i = input - 1; i &gt; 1; i--) {
          result = result * i;
      }
      return result;
  }
  </code></pre>
  <p>But I am getting following errors:</p>
  <pre><code> The prover cannot establish an assertion (LoopInvariantBeforeLoop) in method calculateFactorial
   //@ loop_invariant i &lt; input &amp;&amp; i &gt; 1;
          ^
  MathProblems.java:29: verify: The prover cannot establish an assertion 
  (LoopInvariant) in method calculateFactorial
      //@ loop_invariant i &lt; input &amp;&amp; i &gt; 1;
          ^
  MathProblems.java:31: verify: The prover cannot establish an assertion 
  (ArithmeticOperationRange) in method calculateFactorial: int multiply overflow
          result = result * i;
  </code></pre>
  <p>Could someone help me figure out how to do this the correct way?</p>
  <p>I updated to:</p>
  <pre><code>//@ requires input &lt; 21;
  //@ requires input &gt;= 0;
  //@ requires \forall long i; i == - 1; i &gt; 0;
  //@ ensures \result &gt;= 0;
  //@ signals (Exception) input &gt; 20;
  public /*@ pure @*/ long calculateFactorial(long input) throws Exception {
      long result = 1;
      if (input &lt;= 0) {
          return result;
      }
      else if (input &gt; 20) {
         throw new Exception();
      }
      result = input;
  
      //@ loop_invariant i &lt; input &amp;&amp; i &gt; 0;
      //@ loop_decreases i - 1;
      for (long i = input - 1; i &gt; 1; i--) {
          //@ ensures result == \old(result) * i;
          result = result * i;
      }
      return result;
  }
  </code></pre>
  <p>and now I am getting:</p>
  <pre><code> warning: A refining statement is required for statement specifications
          //@ ensures result == \old(result) * i;
  </code></pre>
  <p>If I put this above, then I get an error the cannot find symbol <code>i</code> :(</p>