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
download ZIP archive