// ------------------------------------------------------------------
//
// Prog.java
// verification of linear search in the RISC ProgramExplorer
//
// (c) 2019, Wolfgang Schreiner: Thinking Programs.
//
// ------------------------------------------------------------------
class Prog
{
  public static int search(int[] a, int x) /*@
    requires (VAR a).null = FALSE;
    ensures 
      LET result = VALUE@NEXT, n = (VAR a).length IN
      IF FORALL(k: INT): 0 <= k AND k < n => (VAR a).value[k] /= VAR x THEN
        result = -1      
      ELSE
         0 <= result AND result < n AND
         (FORALL(k: INT): 0 <= k AND k < result => 
           (VAR a).value[k] /= VAR x) AND
         (VAR a).value[result] = VAR x
      ENDIF;
  @*/
  {
    int n = a.length;
    int r = -1;
    int i = 0;
    while (i < n && r == -1) /*@
      invariant (VAR a).null = FALSE AND VAR n = (VAR a).length
            AND 0 <= VAR i AND VAR i <= VAR n
            AND (FORALL(k: INT): 0 <= k AND k < VAR i => 
                  (VAR a).value[k] /= VAR x)
            AND (VAR r = -1 OR (VAR r = VAR i AND VAR i < VAR n AND 
                   (VAR a).value[VAR r] = VAR x));
      decreases IF VAR r = -1 THEN VAR n - VAR i ELSE 0 ENDIF;  
    @*/
    {
      if (a[i] == x)
        r = i;
      else
        i = i+1;
    }
    return r;
  }
}
// ------------------------------------------------------------------
// end of file
// ------------------------------------------------------------------