// ------------------------------------------------------------------
//
// prog.txt
// specification and verification of linear search in RISCAL
//
// (c) 2019, Wolfgang Schreiner: Thinking Programs.
//
// ------------------------------------------------------------------

val N:ℕ; // size of array
val M:ℕ; // upper bound for elements in array

type int = ℤ[-1,N];
type elem = ℕ[M];
type array = Array[N,elem];

proc search(a:array, x:elem): int
  ensures 
    if ¬∃k:int with 0 ≤ k ∧ k < N. a[k] = x then
      result = -1
    else
      0 ≤ result ∧ result < N ∧
      a[result] = x ∧ ∀k:int with 0 ≤ k ∧ k < result. a[k] ≠ x;
{
  var i:int = 0;
  var r:int = -1;
  while i < N ∧ r = -1 do
    invariant 0 ≤ i ∧ i ≤ N;
    invariant ∀k:int. 0 ≤ k ∧ k < i ⇒ a[k] ≠ x;
    invariant r = -1 ∨ (r = i ∧ i< N ∧ a[r] = x);
    decreases if r = -1 then N-i else 0;
  {
    if a[i] = x
      then r ≔ i;
      else i ≔ i+1;
  }
  return r;
}

// ------------------------------------------------------------------
// end of file
// ------------------------------------------------------------------