## Searching a zero in an array where values never decrease by more than one

Authors: Jean-Christophe Filliâtre

Topics: Array Data Structure

Tools: Why3

see also the index (by topic, by tool, by reference, by year)

```(*
We look for the first occurrence of zero in an array of integers.
The values have the following property: they never decrease by more than one.
The code makes use of that property to speed up the search.
*)

module Decrease1

use int.Int
use ref.Ref
use array.Array

predicate decrease1 (a: array int) =
forall i: int. 0 <= i < length a - 1 -> a[i+1] >= a[i] - 1

let rec lemma decrease1_induction (a: array int) (i j: int) : unit
requires { decrease1 a }
requires { 0 <= i <= j < length a }
ensures  { a[j] >= a[i] + i - j }
variant  { j - i }
= if i < j then decrease1_induction a (i+1) j

let search (a: array int)
requires { decrease1 a }
ensures  {
(result = -1 /\ forall j: int. 0 <= j < length a -> a[j] <> 0)
\/ (0 <= result < length a /\ a[result] = 0 /\
forall j: int. 0 <= j < result -> a[j] <> 0) }
= let i = ref 0 in
while !i < length a do
invariant { 0 <= !i }
invariant { forall j: int. 0 <= j < !i -> j < length a -> a[j] <> 0 }
variant   { length a - !i }
if a[!i] = 0 then return !i;
if a[!i] > 0 then i := !i + a[!i] else i := !i + 1
done;
-1

let rec search_rec (a: array int) (i : int)
requires { decrease1 a /\ 0 <= i }
ensures  {
(result = -1 /\ forall j: int. i <= j < length a -> a[j] <> 0)
\/ (i <= result < length a /\ a[result] = 0 /\
forall j: int. i <= j < result -> a[j] <> 0) }
variant { length a - i }
= if i < length a then
if a[i] = 0 then i
else if a[i] > 0 then search_rec a (i + a[i])
else search_rec a (i + 1)
else
-1

end
```