## Extract non-zero values from an array

This is a Why3 version of a small verification challenge originally in Java and proposed by Peter Müller.

Given an array of integers, we first count how many non-zero values it contains. Then we allocate a new array with exactly this size and we fill it with the non-zero values. The challenge was the handling of a predicate which denotes the number of elements satisfying a given predicate.

In JML, a special construct `\num_of` exists for that purpose, but supporting it is hard because: it must be generic, that is it applies to array of any type; higher-order, because it takes a predicate as parameter; and recursively defined, which is typically hard to handle by automated provers.

The solution presented here use the cloning feature of Why3 to parameterize the theory of `num_of`. an axiomatization encodes the recursive nature of its definition, and a few general lemmas, that can be proved in Coq using induction of Z, are stated to allow SMT solvers to achieve the proof.

Authors: Jean-Christophe Filliâtre

Topics: Array Data Structure

Tools: Why3

See also: Filter elements of an array

see also the index (by topic, by tool, by reference, by year)

```(* A small verification challenge proposed by Peter Müller.

Given an array of integers, we first count how many non-zero values
it contains. Then we allocate a new array with exactly this size and
we fill it with the non-zero values. *)

module Muller

use int.Int
use ref.Refint
use array.Array
use int.NumOf as N

function numof (a: array int) (l u: int) : int =
N.numof (fun i -> a[i] <> 0) l u

let compact (a: array int) =
let count = ref 0 in
for i = 0 to length a - 1 do
invariant { !count = numof a 0 i }
if a[i] <> 0 then incr count
done;
let u = make !count 0 in
count := 0;
for i = 0 to length a - 1 do
invariant { !count = numof a 0 i }
if a[i] <> 0 then begin u[!count] <- a[i]; incr count end
done

end
```