Wiki Agenda Contact English version

FoVeOOS'11 Competition: challenge 3, in Java

Find two duplets in an array, in Java


Auteurs: Claude Marché

Catégories: Array Data Structure

Outils: Krakatoa / Why3

Références: The COST FoVeOOS'11 Competition

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


/*
COST Verification Competition. vladimir@cost-ic0701.org

Challenge 3: Two equal elements

Given: An integer array a of length n+2 with n>=2. It is known that at
least two values stored in the array appear twice (i.e., there are at
least two duplets).

Implement and verify a program finding such two values.

You may assume that the array contains values between 0 and n-1.
*/


class Integer {
    int value;
    /*@ ensures this.value == a;
      @*/
    Integer(int a) {
        value = a;
    }
}

class Pair {
    int x,y;
    /*@ ensures this.x == a && this.y == b;
      @*/
    Pair(int a,int b) {
        x = a; y = b;
    }
}

class Quadruple {
    int x,y,z,t;
    /*@ ensures this.x == a && this.y == b &&
      @         this.z == c && this.t == d;
      @*/
    Pair(int a,int b,int c,int d) {
        x = a; y = b; z = c; t = d;
    }
}

/* equality between an integer and a possibly null Integer object */
/*@ predicate eq_opt{L}(integer x, Integer o) =
  @   o != null && x == o.value;
  @*/

/* A duplet in array a is a pair of indexes (i,j) in the bounds of array
   a such that a[i] = a[j] */
/*@ predicate is_duplet{L}(int a[], integer i, integer j) =
  @    0 <= i < j < a.length && a[i] == a[j];
  @*/

class Duplets {

    /* duplet(a) returns the indexes (i,j) of a duplet in a.
     * moreover, if except is not null, the value of this duplet must
     * be different from it.
     */
    /*@ requires 2 <= a.length &&
      @   \exists integer i j;
      @     is_duplet(a,i,j) && ! eq_opt(a[i],except) ;
      @ ensures
      @   is_duplet(a,\result.x,\result.y) &&
      @   ! eq_opt(a[\result.x],except); 
      @*/
    Pair duplet(int a[], Integer except) {
        /*@ loop_invariant
          @  \forall integer k l; 0 <= k < i && k < l < a.length ==>
          @    ! eq_opt(a[k],except) ==> ! is_duplet(a,k,l);
          @ loop_variant a.length - i;
          @*/
        for(int i=0; i <= a.length - 2; i++) {
            int v = a[i];
            if (except != null && except.value != v) {
                /*@ loop_invariant
                  @   \forall integer l; i < l < j ==> ! is_duplet(a,i,l);
                  @ loop_variant a.length - j;
                  @*/
                for (int j=i+1; j < a.length; j++) {
                    if (a[j] == v) {
                        return new Pair(i, j);
                    }
                }
            }
        }
        // assert \forall integer i j; ! is_duplet(a,i,j);
        //@ assert false;
        return null;
    }


    /* requires 4 <= a.length && \exists integer i j k l;
      @   is_duplet(a,i,j) && is_duplet(a,k,l) && a[i] != a[k];
      @ ensures is_duplet(a,\result.x,\result.y) &&
      @   is_duplet(a,\result.z,\result.t) &&
      @   a[\result.x] != a[\result.z];
      @*/
    Quadruple duplets(int a[]) {
        Pair p = duplet(a,null);
        Pair q = duplet(a,new Integer(a[p.x]));
        return new Quadruple(p.x,p.y,q.x,q.y);
    }
   

}

/*
Local Variables:
compile-command: "make Duplets.why3ml"
End:
*/