decrease1.mlw 1.6 KB
Newer Older
1 2 3 4 5 6 7 8 9 10

(*
  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 import int.Int
11 12
  use import ref.Ref
  use import array.Array
13

Andrei Paskevich's avatar
Andrei Paskevich committed
14
  predicate decrease1 (a: array int) =
15
    forall i: int. 0 <= i < length a - 1 -> a[i+1] >= a[i] - 1
16 17 18 19 20

  lemma decrease1_induction:
    forall a: array int. decrease1 a ->
    forall i j: int. 0 <= i <= j < length a -> a[j] >= a[i] + i - j

21
  exception Found
22

23 24 25 26 27 28 29
  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
30 31
    try
      while !i < length a do
32 33
        invariant { 0 <= !i }
        invariant { forall j: int. 0 <= j < !i -> j < length a -> a[j] <> 0 }
34
        variant   { length a - !i }
35 36
        if a[!i] = 0 then raise Found;
        if a[!i] > 0 then i := !i + a[!i] else i := !i + 1
37 38
      done;
      -1
39
    with Found ->
40 41 42
      !i
    end

43 44 45
  let rec search_rec (a: array int) (i : int)
    requires { decrease1 a /\ 0 <= i }
    ensures  {
46 47 48 49
         (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 }
50
  = if i < length a then
51
      if a[i] = 0 then i
52
      else if a[i] > 0 then search_rec a (i + a[i])
53 54 55
      else search_rec a (i + 1)
    else
      -1
56 57

end