package intset_model;

//@ axiom mean1 : (\forall int x,y ; x <= y ; x <= (x + y) / 2) ;
//@ axiom mean2 : (\forall int x,y ; x < y ; (x + y) / 2 < y) ;

//@ logic type intset ;

//@ predicate In(int n, intset s) ;

//@ logic intset union(intset s1, intset s2) ;
//@ logic intset singleton(int n) ;

/*@ axiom In_union : 
  @   (\forall intset s1,s2 ; (\forall int n ; 
  @      In(n,union(s1,s2)) <==> In(n,s1) || In(n,s2))) ;
  @*/

/*@ axiom In_singleton : 
  @   (\forall int n,k ; 
  @      In(n,singleton(k)) <==> n==k) ;
  @*/

/*@ axiom intset_ext : 
  @   (\forall intset s1,s2 ; 
  @      (\forall int n ; In(n,s1) <==> In(n,s2)) ==> s1==s2) ;
  @*/

/*@ predicate array_models(intset s, int t[], int i, int j) {
  @   t != null && 
  @   0 <= i && j < t.length &&
  @   (\forall int n; In(n,s) <==> 
  @      (\exists int k; 
  @         i <= k && k <= j ; n==t[k]))
  @ }
  @*/

/*@ predicate IntSet_models(intset s, IntSet this) {
  @   this != null && 
  @   array_models(s,this.t,0,this.size-1) 
  @ }
  @*/

public class IntSet {

    int size = 0;
    int t[] = new int[10];

    /*@ private invariant
      @   t != null && 0 <= size && size <= t.length &&
      @   (\forall int i,j; 0 <= i && i <= j && j < size; t[i] <= t[j]);
      @*/

    /*@ public normal_behavior
      @   modifiable \nothing;
      @   ensures
      @     0 <= \result && \result <= size &&
      @     (\forall int i; 0 <= i && i < \result; t[i] < n) && 
      @     (\forall int i; \result <= i && i < size; t[i] >= n) ;
      @*/
    public int index(int n) {
	int a = 0, b = size, m;
	/*@ loop_invariant 
	  @   0 <= a && a <= b && b <= size &&
	  @   (\forall int i; 0 <= i && i < a; t[i] < n) && 
	  @   (\forall int i; b <= i && i < size; t[i] >= n) ; 
	  @ decreases b-a;
	  @*/
	while (a<b) {
	    m = (a+b)/2;
	    if (t[m] < n) a=m+1; else b=m;
	}
	return a;
    }

    /*@ public normal_behavior
      @   modifiable \nothing;
      @   ensures 
      @     (\forall intset s; IntSet_models(s,this) ;
      @          \result <==> In(n,s));
      @*/
    public boolean mem(int n) {
	int i = index(n);
	return (i < size && t[i] == n);
    }	
        
    /* add with intermediate annotations for automatic
     * proof with simplify 
     */
    /*@ public normal_behavior
      @   modifiable t,size,t[*];
      @   ensures
      @    (\forall intset s; \old(IntSet_models(s,this)) ;
      @       IntSet_models(union(s,singleton(n)),this)) ;
      @ */
    public void add(int n) {	
	int i = index(n);
	if (i < size && t[i] == n) return;
        /*@ modifies t,t[*];
            ensures (\forall int j; 0 <= j && j < i; t[j]==\old(t[j])) 
              && (\forall int j; i+1 <= j && j < size + 1; t[j]==\old(t[j-1]))
              && (\forall int j; i <= j && j < size; \old(t[j])==t[j+1])
              && t !=null && t[i]==n && size < t.length && t instanceof int[];
        */
	{if (size < t.length) {
	    copy(t,t,i,size-1,i+1);
	}
	else {
	    int old[] = t;
	    t = new int[2*size+1];
	    copy(old,t,0,i-1,0);
	    copy(old,t,i,size-1,i+1);
	}
	t[i] = n;};
	size++; 
    }


    /*
       copy(src,dest,a,b,c) copies src[a..b] to dest[c..c+b-a]
       if src and dest are the same, c is assumed greater than or equal to a.
     */
    /*@ public normal_behavior
      @   requires src != null && dest != null && 
      @   0 <= a && a-1 <= b && b < src.length && 0 <= c && 
      @     c+b-a < dest.length && (dest == src ==> c >= a);
      @   assignable dest[c..c+b-a]; 
      @   ensures (\forall int i; c <= i && i <= c+b-a; dest[i] == \old(src[i+a-c]));
      @*/

    public static void copy(int src[], int dest[],int a, int b, int c) {
	/*@ loop_invariant 
	  @   a-1 <= j && j <= b &&
	  @      (\forall int i; j < i && i <= b; dest[i+c-a] == \old(src[i])) &&
	  @      (\forall int i; c <= i && i <= j+c-a ; dest[i] == \old(dest[i]));
	  @ decreases j;
	  @*/
	for (int j = b; j >= a; j--) {
	    dest[j+c-a] = src[j];
	}
    }
}