examples/zeros.mlw

   1
   2 (** Setting all the elements of an array to zero *)
   3
   4 module SetZeros
   5
   6   use int.Int
   7   use array.Array
   8
   9   let set_zeros (a : array int) =
  10     ensures { forall j: int. 0 <= j < a.length -> a[j] = 0 }
  11     for i = 0 to a.length - 1 do
  12       invariant { forall j: int. 0 <= j < i -> a[j] = 0 }
  13       a[i] <- 0
  14     done
  15
  16   let harness () =
  17     let a0 = make 42 1 in
  18     set_zeros a0;
  19     assert { length a0 = 42 };
  20     assert { a0[12] = 0 }
  21
  22 end
  23
  24 (** Checking that an array contains only zeros *)
  25
  26 module AllZeros
  27
  28   use int.Int
  29   use array.Array
  30   use ref.Refint
  31
  32   predicate all_zeros (a: array int) (hi: int) =
  33     forall i: int. 0 <= i < hi -> a[i] = 0
  34
  35   (** with a for loop (a bit naive, since it always scans the whole array) *)
  36
  37   let all_zeros1 (a: array int) : bool
  38     ensures { result <-> all_zeros a a.length }
  39   =
  40     let res = ref True in
  41     for i = 0 to length a - 1 do
  42       invariant { !res <-> all_zeros a i }
  43       if a[i] <> 0 then res := False
  44     done;
  45     !res
  46
  47   (** with a while loop, stopping as early as possible *)
  48
  49   let all_zeros2 (a: array int) : bool
  50     ensures { result <-> all_zeros a a.length }
  51   =
  52     let res = ref True in
  53     let i = ref 0 in
  54     while !res && !i < length a do
  55       invariant { 0 <= !i <= a.length }
  56       invariant { !res <-> all_zeros a !i }
  57       variant   { a.length - !i }
  58       res := (a[!i] = 0);
  59       incr i
  60     done;
  61     !res
  62
  63   (** no need for a Boolean variable, actually *)
  64
  65   let all_zeros3 (a: array int) : bool
  66     ensures { result <-> all_zeros a a.length }
  67   =
  68     let i = ref 0 in
  69     while !i < length a && a[!i] = 0 do
  70       invariant { 0 <= !i <= a.length }
  71       invariant { all_zeros a !i }
  72       variant   { a.length - !i }
  73       incr i
  74     done;
  75     !i = length a
  76
  77   (** with a recursive function *)
  78
  79   let all_zeros4 (a: array int) : bool
  80     ensures { result <-> all_zeros a a.length }
  81   =
  82     let rec check_from (i: int) : bool
  83       requires { 0 <= i <= a.length }
  84       requires { all_zeros a i }
  85       variant  { a.length - i }
  86       ensures  { result <-> all_zeros a a.length }
  87     = i = length a || a[i] = 0 && check_from (i+1)
  88     in
  89     check_from 0
  90
  91   (** divide-and-conqueer *)
  92
  93   predicate zero_interval (a: array int) (lo hi: int) =
  94     forall i: int. lo <= i < hi -> a[i] = 0
  95
  96   use int.ComputerDivision
  97
  98   let all_zeros5 (a: array int) : bool
  99     ensures { result <-> all_zeros a a.length }
 100   =
 101     let rec check_between (lo hi: int) : bool
 102       requires { 0 <= lo <= hi <= a.length }
 103       variant  { hi - lo }
 104       ensures  { result <-> zero_interval a lo hi }
 105     =
 106       hi <= lo ||
 107       let mid = lo + div (hi - lo) 2 in
 108       a[mid] = 0 && check_between lo mid && check_between (mid+1) hi
 109     in
 110     check_between 0 (Array.length a)
 111
 112 end