// 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 ∧ r < 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);