why3/examples/zeros.mlw

(** Setting all the elements of an array to zero *)

module SetZeros

  use int.Int
  use array.Array

  let set_zeros (a : array int) =
    ensures { forall j: int. 0 <= j < a.length -> a[j] = 0 }
    for i = 0 to a.length - 1 do
      invariant { forall j: int. 0 <= j < i -> a[j] = 0 }
      a[i] <- 0
    done

  let harness () =
    let a0 = make 42 1 in
    set_zeros a0;
    assert { length a0 = 42 };
    assert { a0[12] = 0 }

end

(** Checking that an array contains only zeros *)

module AllZeros

  use int.Int
  use array.Array
  use ref.Refint

  predicate all_zeros (a: array int) (hi: int) =
    forall i: int. 0 <= i < hi -> a[i] = 0

  (** with a for loop (a bit naive, since it always scans the whole array) *)

  let all_zeros1 (a: array int) : bool
    ensures { result <-> all_zeros a a.length }
  =
    let res = ref True in
    for i = 0 to length a - 1 do
      invariant { !res <-> all_zeros a i }
      if a[i] <> 0 then res := False
    done;
    !res

  (** with a while loop, stopping as early as possible *)

  let all_zeros2 (a: array int) : bool
    ensures { result <-> all_zeros a a.length }
  =
    let res = ref True in
    let i = ref 0 in
    while !res && !i < length a do
      invariant { 0 <= !i <= a.length }
      invariant { !res <-> all_zeros a !i }
      variant   { a.length - !i }
      res := (a[!i] = 0);
      incr i
    done;
    !res

  (** no need for a Boolean variable, actually *)

  let all_zeros3 (a: array int) : bool
    ensures { result <-> all_zeros a a.length }
  =
    let i = ref 0 in
    while !i < length a && a[!i] = 0 do
      invariant { 0 <= !i <= a.length }
      invariant { all_zeros a !i }
      variant   { a.length - !i }
      incr i
    done;
    !i = length a

  (** with a recursive function *)

  let all_zeros4 (a: array int) : bool
    ensures { result <-> all_zeros a a.length }
  =
    let rec check_from (i: int) : bool
      requires { 0 <= i <= a.length }
      requires { all_zeros a i }
      variant  { a.length - i }
      ensures  { result <-> all_zeros a a.length }
    = i = length a || a[i] = 0 && check_from (i+1)
    in
    check_from 0

  (** divide-and-conqueer *)

  predicate zero_interval (a: array int) (lo hi: int) =
    forall i: int. lo <= i < hi -> a[i] = 0

  use int.ComputerDivision

  let all_zeros5 (a: array int) : bool
    ensures { result <-> all_zeros a a.length }
  =
    let rec check_between (lo hi: int) : bool
      requires { 0 <= lo <= hi <= a.length }
      variant  { hi - lo }
      ensures  { result <-> zero_interval a lo hi }
    =
      hi <= lo ||
      let mid = lo + div (hi - lo) 2 in
      a[mid] = 0 && check_between lo mid && check_between (mid+1) hi
    in
    check_between 0 (Array.length a)

end