examples/decrease1.mlw

   1
   2 (*
   3   We look for the first occurrence of zero in an array of integers.
   4   The values have the following property: they never decrease by more than one.
   5   The code makes use of that property to speed up the search.
   6 *)
   7
   8 module Decrease1
   9
  10   use int.Int
  11   use ref.Ref
  12   use array.Array
  13
  14   predicate decrease1 (a: array int) =
  15     forall i: int. 0 <= i < length a - 1 -> a[i+1] >= a[i] - 1
  16
  17   let rec lemma decrease1_induction (a: array int) (i j: int) : unit
  18     requires { decrease1 a }
  19     requires { 0 <= i <= j < length a }
  20     ensures  { a[j] >= a[i] + i - j }
  21     variant  { j - i }
  22   = if i < j then decrease1_induction a (i+1) j
  23
  24   let search (a: array int)
  25     requires { decrease1 a }
  26     ensures  {
  27        (result = -1 /\ forall j: int. 0 <= j < length a -> a[j] <> 0)
  28     \/ (0 <= result < length a /\ a[result] = 0 /\
  29         forall j: int. 0 <= j < result -> a[j] <> 0) }
  30   = let i = ref 0 in
  31     while !i < length a do
  32       invariant { 0 <= !i }
  33       invariant { forall j: int. 0 <= j < !i -> j < length a -> a[j] <> 0 }
  34       variant   { length a - !i }
  35       if a[!i] = 0 then return !i;
  36       if a[!i] > 0 then i := !i + a[!i] else i := !i + 1
  37     done;
  38     -1
  39
  40   let rec search_rec (a: array int) (i : int)
  41     requires { decrease1 a /\ 0 <= i }
  42     ensures  {
  43          (result = -1 /\ forall j: int. i <= j < length a -> a[j] <> 0)
  44       \/ (i <= result < length a /\ a[result] = 0 /\
  45           forall j: int. i <= j < result -> a[j] <> 0) }
  46     variant { length a - i }
  47   = if i < length a then
  48       if a[i] = 0 then i
  49       else if a[i] > 0 then search_rec a (i + a[i])
  50       else search_rec a (i + 1)
  51     else
  52       -1
  53
  54 end