A method finding an element in an integer array, returning -1 if the element has not been found. The source code includes the JML specification covering all facts that our strength analysis tool discovered.

Find.java

public class Find {
    //@ ghost int f_iLastRun;
    
    // Everything covered
    /*@ public normal_behavior
      @ ensures
      @      ((\exists int i; i >= 0 && i < arr.length; arr[i] == n) ==>
      @          (arr[\result] == n && \result == f_iLastRun)
      @      )
      @   && ((\forall int i; i >= 0 && i < arr.length; arr[i] != n) ==> \result == -1)
      @   ;
      @ assignable f_iLastRun;
      @*/
    public int find(int[] arr, int n) {
        int i = 0;
        int result = -1;
      
        //@ set f_iLastRun = i - 1;

        /*@ loop_invariant
          @      i >= 0 && i <= arr.length
          @   && i == f_iLastRun + 1
          @   && (result != -1 || (\forall int k; k >= 0 && k < i; arr[k] != n))
          @   && (result == -1 || arr[result] == n && result == i-1)
          @   ;
          @ decreases arr.length - i;
          @ assignable f_iLastRun;
          @*/
        while (result == -1 && i < arr.length) {
            //@ set f_iLastRun = i;
            if (arr[i] == n) {
                result = i;
            }

            i++;
        }

        return result;
    }
}