Contact Version française

The ProVal team was stopped at the end of August 2012, and reborn into a new team Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.

Filter elements of an array

Extraction of positive values from an array of integers.


Authors: Claude Marché

Topics: Array Data Structure / Separation challenges

Tools: Krakatoa / Coq

References: The VerifyThis Benchmarks

See also: Extract non-zero values from an array

index


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