class A
{
   //@ requires a != null;
   //@ requires (i >= 0) && (i < a.length);
   //@ requires (j >= 0) && (j < a.length);
   //@ modifies a[i];
   //@ modifies a[j];
   //@ ensures \old(a[i]) == a[j] && \old(a[j]) == a[i]; // swap swaps
   //@ ensures (\forall int i1; i1 >= 0 && i1 < a.length ==>  (\exists int i2; (i2 >= 0) && (i2 < a.length) && (\old(a)[i1] == a[i2]) ) ); // swap semi-permutes, this is not enough for multisets
   void swap(int[] a, int i, int j)
   {
      int d;
      d = a[j];
      a[j] = a[i];
      a[i] = d;
   }

   //@ requires a != null;
   //@ modifies a[*];
   //@ ensures (\forall int i1; (i1 >= 0) && (i1 < a.length - 1); (a[i1] <= a[i1 + 1]));
   void bubble(int[] a)
   {
       /* Bubble sort version that doesn't detect whether the array is already sorted, but decreases the upper bound index(variable "k"),
          The varible "k" would most likely be needed even if the optimalization hadn't been implemented to show correctness.
       */
   
       int i,k;
       
       k = a.length;
       //@ loop_invariant k <= a.length; //The loop starts with k == a.length
       //@ loop_invariant k >= 0;        //k is decreased until 0 is reached or the array is sorted

        // all in a[k..lenght-1] are uppers bound for a[0..k-1]
       //@ loop_invariant (\forall int i1, i2; (i2 >= 0) && (i2 < k) && (i1 >= k) && (i1 < a.length); (a[i1] >= a[i2]));
       
       //@ loop_invariant (k == a.length) || (\forall int i1; (i1 > k) && (i1 < a.length); (a[k] <= a[i1])); //This is weaker then the next one, but Simplify needs it, the k==len is unnecessary because i1<len is false then.
       //@ loop_invariant (\forall int i1; (i1 >= k) && (i1 < a.length - 1) ==> (a[i1] <= a[i1 + 1]));//a[k..lenght - 1] is sorted
       while (k > 0)
       {
         i = 0;
	 //@ loop_invariant (i >= 0) && (i <= a.length);
	 //@ loop_invariant (\forall int j; (j >= 0) && (j < i) ==> a[j] <= a[i]);
	 //@ loop_invariant (i >= 0) && (i < k);

	 /*  The next two invariants are actually invariants of the outter loop. 
	     And it's quite obvious that they will not be broken because the array fields in question are not modified.
	 */    
	 //@ loop_invariant (\forall int i1, i2; (i2 >= 0) && (i2 < k) && (i1 >= k) && (i1 < a.length) ==> (a[i1] >= a[i2]));
	 //@ loop_invariant (\forall int i1; (i1 >= k) && (i1 < a.length - 1) ==> (a[i1] <= a[i1 + 1])); 
	 while (i <  k - 1)
	 {  
	    if (a[i] > a[i + 1]) 
	       swap(a, i, i + 1);
	    
	    i = i + 1;
	 }
	 	 
	 k = k - 1;
       }
   }
   
   //@ requires a != null;
   //@ modifies a[*];
   //@ ensures (\forall int i1; (i1 >= 0) && (i1 < a.length - 1) ==> (a[i1] <= a[i1 + 1]));
   void bubble1(int[] a)
   {
       /* Bubble sort with change detection and the upper index decreasing */
       int k; 
       boolean sorted;

       int i;  
       
       k = a.length;
       sorted = false;
       
       //@ loop_invariant k >= 0 && k <= a.length;
       
       // all in a[k..lenght-1] are uppers bound for a[0..k-1]
       //@ loop_invariant (\forall int i1, i2; (i2 >= 0) && (i2 < k) && (i1 >= k) && (i1 < a.length) ==> (a[i1] >= a[i2])); 
      
       //a[k] is a lower bound for a[k+1..len-1]
       //(it is weaker then the next one, but Simplify needs it)
       //@ loop_invariant (\forall int i1; (i1 > k) && (i1 < a.length) ==>  (a[k] <= a[i1])); 

       //@ loop_invariant (\forall int i1; (i1 >= k) && (i1 < a.length - 1) ==> (a[i1] <= a[i1 + 1])); // a[k..lenght - 1] is sorted

       // if sorted=true then the array is sorted
       // (note that the invariant might be broken for a while inside the loop body, but it will be restored at the end
       //@ loop_invariant sorted ==> (\forall int i1; (i1 >= 0) && (i1 < a.length - 1) ==> a[i1] <= a[i1 + 1]); 
       while (!sorted && k > 0)
       {
         i = 0;
	 sorted = true;// assume that the array is sorted
	 
	 //@ loop_invariant (i >= 0) && (i <= a.length);
	 //@ loop_invariant (\forall int j; (j >= 0) && (j < i) ==> a[j] <= a[i]); //the greatest value bubbles up
	 //@ loop_invariant (i >= 0) && (i <= k - 1);
	    //sorted implies a[0..i] is sorted
	 //@ loop_invariant sorted ==> (\forall int i1; (i1 >= 0) && (i1 < i) ==> a[i1] <= a[i1 + 1]);

	 /*  The next two invariants are actually invariants of the outter loop. 
	     And it's quite obvious that they will not be broken because the array fields in question are not modified.
	 */    
	 //@ loop_invariant (\forall int i1, i2; (i2 >= 0) && (i2 < k) && (i1 >= k) && (i1 < a.length) ==> (a[i1] >= a[i2]));
	 //@ loop_invariant (\forall int i1; (i1 >= k) && (i1 < a.length - 1) ==> (a[i1] <= a[i1 + 1])); 
	 while (i <  k - 1)
	 {  
	    if (a[i] > a[i + 1]) 
	    {
	       swap(a, i, i + 1);
	       sorted = false; //we no longer can assume that the array is sorted
	    }
	    
	    i = i + 1;
	 }
	 	 
	 k = k - 1;
       }
   }
}