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;
}
}