// linear search: given an array a and key x, 
// return the smallest position r where x occurs in a 
// (r = -1, if x does not occur in a)

val N:ℕ;
val M:ℕ;

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

proc search(a:array, x:elem): index
  ensures 
    (result = -1 ∧ ∀i:index. 0 ≤ i ∧ i < N ⇒ a[i] ≠ x) ∨
    (0 ≤ result ∧ result < N ∧ 
      a[result] = x ∧ ∀i:index. 0 ≤ i ∧ i < result ⇒ a[i] ≠ x);
{
  var i:index = 0;
  var r:index = -1;
  while i < N ∧ r = -1 do
    invariant 0 ≤ i ∧ i ≤ N;
    invariant ∀j:index. 0 ≤ j ∧ j < i ⇒ a[j] ≠ 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;
}

// the verification conditions to be proved
// for the total correctness of the program

pred Input(i:index, r:index) ⇔ 
  i = 0 ∧ r = -1;

pred Output(a:array, x:elem, i:index, r:index) ⇔
  (r = -1 ∧ ∀i:index. 0 ≤ i ∧ i < N ⇒ a[i] ≠ x) ∨
  (0 ≤ r ∧ r < N ∧ a[r] = x ∧ ∀i:index. 0 ≤ i ∧ i < r ⇒ a[i] ≠ x);

pred Invariant(a:array, x:elem, i:index, r:index) ⇔
  0 ≤ i ∧ i ≤ N ∧
  (∀j:index. 0 ≤ j ∧ j < i ⇒ a[j] ≠ x) ∧
  (r = -1 ∨ (r = i ∧ i < N ∧ a[r] = x));
 
fun Termination(a:array, x:elem, i:index, r:index): index =
  if r = -1 then N-i else 0;

theorem A(a:array, x:elem, i:index, r:index) ⇔
  Input(i, r) ⇒ Invariant(a, x, i, r);
  
theorem T(a:array, x:elem, i:index, r:index) ⇔
  Invariant(a, x, i, r) ⇒ Termination(a, x, i, r) ≥ 0;

theorem B1(a:array, x:elem, i:index, r:index) ⇔
  Invariant(a, x, i, r) ∧ i < N ∧ r = -1 ∧ a[i] = x ⇒
    Invariant(a, x, i, i) ∧ 
    Termination(a, x, i, i) < Termination(a, x, i, r);
  
theorem B2(a:array, x:elem, i:index, r:index) ⇔
  Invariant(a, x, i, r) ∧ i < N ∧ r = -1 ∧ a[i] ≠ x ⇒
    Invariant(a, x, i+1, r) ∧ 
    Termination(a, x, i+1, r) < Termination(a, x, i, r);
  
theorem C(a:array, x:elem, i:index, r:index) ⇔
  Invariant(a, x, i, r) ∧ ¬(i < N ∧ r = -1) ⇒
    Output(a, x, i, r);



