(** 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