## Filter elements of an array

Extraction of positive values from an array of integers.

**Authors:** Claude Marché

**Topics:** Array Data Structure / Separation challenges

**References:** The VerifyThis Benchmarks

**See also:** Extract non-zero values from an array

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

## Description

This small program was originally proposed by Peter Müller.

The source code is as follows. Given an array of integers, we first
count how many positive values it contains. Then we allocate a new
array with exactly this size and we fill it with the positive values.
The original challenge was how to specify the behavior, and in
particular the support for a construct that counts the number of
elements of an array satisfying a given predicate, like
`\numof`

. Another challenge is to prove that the second loop does
not make any access out of bounds.

## Proof via Separation Analysis

The Java file below can be analyzed by Krakatoa/Why using

gwhy Muller.java

Verification conditions are proved by most SMT solvers, except the lemmas which need induction and can be proved in Coq.

One should notice the pragma `//@+ SeparationPolicy = Regions`

given at the beginning of the file. This turns on a static analysis of
separation [1] of references, which allows to build
simpler VCs. With this analysis, it is statically known that the array `u`

is disjoint from array `t`

and thus
the memory model used for generating VCs statically incorporates the fact that updated the cells of `u`

does not change
the predicate `count = num_of_pos(0,i,t)`

which is needed to prove safety.

## References

- [1]
- Thierry Hubert and Claude Marché. Separation analysis for deductive verification. Technical report, Université Paris XI, 2007. http://www.lri.fr/~marche/separation.pdf.

## Source code

//@+ SeparationPolicy = Regions /*@ axiomatic NumOfPos { @ logic integer num_of_pos{L}(integer i,integer j,int t[]); @ axiom num_of_pos_empty{L} : @ \forall integer i j, int t[]; @ i >= j ==> num_of_pos(i,j,t) == 0; @ axiom num_of_pos_true_case{L} : @ \forall integer i j k, int t[]; @ i < j && t[j-1] > 0 ==> @ num_of_pos(i,j,t) == num_of_pos(i,j-1,t) + 1; @ axiom num_of_pos_false_case{L} : @ \forall integer i j k, int t[]; @ i < j && ! (t[j-1] > 0) ==> @ num_of_pos(i,j,t) == num_of_pos(i,j-1,t); @ } @*/ /*@ lemma num_of_pos_non_negative{L} : @ \forall integer i j, int t[]; 0 <= num_of_pos(i,j,t); @*/ /*@ lemma num_of_pos_additive{L} : @ \forall integer i j k, int t[]; i <= j <= k ==> @ num_of_pos(i,k,t) == num_of_pos(i,j,t) + num_of_pos(j,k,t); @*/ /*@ lemma num_of_pos_increasing{L} : @ \forall integer i j k, int t[]; @ j <= k ==> num_of_pos(i,j,t) <= num_of_pos(i,k,t); @*/ /*@ lemma num_of_pos_strictly_increasing{L} : @ \forall integer i n, int t[]; @ 0 <= i < n && t[i] > 0 ==> @ num_of_pos(0,i,t) < num_of_pos(0,n,t); @*/public class Muller{ /*@ requires t != null; @*/ public static int[] m(int t[]) { int count = 0; /*@ loop_invariant @ 0 <= i <= t.length && @ 0 <= count <= i && @ count == num_of_pos(0,i,t) ; @ loop_variant t.length - i; @*/ for (int i=0 ; i < t.length; i++) if (t[i] > 0) count++; int u[] = new int[count]; count = 0; /*@ loop_invariant @ 0 <= i <= t.length && @ 0 <= count <= i && @ count == num_of_pos(0,i,t); @ loop_variant t.length - i; @*/ for (int i=0 ; i < t.length; i++) { if (t[i] > 0) u[count++] = t[i]; } return u; } }