#include "qsorti.h"

#define MAXSTACK 2048		// максимальный размер стека

/*@ predicate Swap{L1,L2}(int* a, integer size, integer i, integer j) =
  @   \at(a[i],L1) == \at(a[j],L2) &&
  @   \at(a[j],L1) == \at(a[i],L2) &&
  @   \forall integer k; 0 <= k < size && k != i && k != j
  @       ==> \at(a[k],L1) == \at(a[k],L2);
  @*/


/*@ axiomatic Permut {
  @   // permut{L1,L2}(t,n) is true whenever t[0..n-1] in state L1
  @   // is a permutation of t[0..n-1] in state L2
  @  predicate permut{L1,L2}(int* t, integer n);
  @    // reads \at(t[..],L1), \at(t[..],L2);
  @  axiom permut_refl{L} :
  @    \forall int* t, integer n; permut{L,L}(t,n);
  @  axiom permut_sym{L1,L2} :
  @    \forall int* t, integer n;
  @      permut{L1,L2}(t,n) ==> permut{L2,L1}(t,n) ;
  @  axiom permut_trans{L1,L2,L3} :
  @    \forall int* t, integer n;
  @      permut{L1,L2}(t,n) && permut{L2,L3}(t,n)
  @      ==> permut{L1,L3}(t,n) ;
  @  axiom permut_exchange{L1,L2} :
  @    \forall int* t, integer i, j, n;
  @       0 <= i < n && 0 <= j < n && Swap{L1,L2}(t, n, i, j)
  @        ==> permut{L1,L2}(t,n);
  @ }
  @*/

/*@predicate sameArray{L1,L2}(int* a, integer size, integer lb, integer ub) =
  @  \forall integer k; ((lb <= ub) && (0 <= k < size) && (k < lb || k > ub)) ==> \at(a[k],L1) == \at(a[k],L2);
  @*/

/*@ predicate is_sorted{L}(int* a, integer low, integer high) =
  @   \forall integer i, j; low <= i <= j <= high ==> a[i] <= a[j];
  @*/

/*@ predicate high_bound{L}(int* a, integer lb, integer i, integer pivot) =
  @		\forall integer i0; lb <= i0 <= i ==> a[i0] <= pivot;
  @*/

/*@ predicate low_bound{L}(int* a, integer j, integer ub, integer pivot) =
  @   	\forall integer j0; j <= j0 <= ub ==> a[j0] >= pivot;
  @*/

/*@ predicate left_part_less{L}(int* a, integer p, integer lb, integer ub) =
  @ 	\forall integer i, j; lb <= i <= p && p <= j <= ub
  @			==> a[i] <= a[j];
 */

/*@ predicate left_part_less_weak{L}(int* a, integer p, integer lb, integer ub) =
  @ 	\forall integer i, j; lb <= i < p && p <= j <= ub
  @			==> a[i] <= a[j];
 */


/*@ predicate retain_sorted_parts{L1,L2}(int* a, integer lb, integer ub) =
  @ 	\forall integer i, j; (lb <= i <= j <= ub && is_sorted{L1}(a, i, j))
  @			==> is_sorted{L2}(a, i, j);
 */

/*@ predicate all_right_elems_bigger{L}(int *a, integer size, integer ub) =
 @		\forall integer i,j; ub < i < size && 0 <= j <= ub ==> a[i] >= a[j];
 */

/*@ predicate all_left_elems_less{L}(int *a, integer size, integer lb) =
 @		\forall integer i,j; 0 <= i < lb && lb <= j < size ==> a[i] <= a[j];
 */

/*@predicate same{L1,L2}(int* stack, integer pos) =
  @  \forall integer k; ((0 <= k < MAXSTACK) && (k < pos)) ==> \at(stack[k],L1) == \at(stack[k],L2);
  @*/

/*@predicate stack_boundaries{L}(int *stack, integer limit_pos, integer min, integer max) =
 @  \forall integer i; ((0 <= i < MAXSTACK && i <= limit_pos) ==> min <= stack[i] <= max);
 */

/*@ predicate good_hole{L}(int* a, int* lbstack, int* ubstack, integer i, integer size) =
@   is_sorted{L}(a, ubstack[i], lbstack[i+1])
@	&& left_part_less{L}(a, ubstack[i]+1, lbstack[i], lbstack[i+1]-1)
@	&& left_part_less{L}(a, lbstack[i+1]-1, ubstack[i]+1, size-1);
 */

//===lemmas===

/*@	lemma mean_property :
  @		\forall integer x,y; x <= y ==> x <= (x+y)/2 <= y;
 */

/*@	lemma low_bound_inductive{L} :
  @		\forall int* a, integer j, ub, pivot;
  @			low_bound{L}(a, j, ub, pivot) && a[j-1] >= pivot
  @				==> low_bound{L}(a, j-1, ub, pivot);
 */

/*@	lemma high_bound_inductive{L} :
  @		\forall int* a, integer lb, i, pivot;
  @			high_bound{L}(a, lb, i, pivot) && a[i+1] <= pivot
  @				==> high_bound{L}(a, lb, i+1, pivot);
 */

//если выполняется low_bound для всех элементов от j до ub, то она выполняется и для a[j]
/*@	lemma low_bound_reverse{L} :
  @		\forall int* a, integer j, ub, pivot;
  @			low_bound{L}(a, j, ub, pivot) && j <= ub
  @				==> a[j] >= pivot;
 */


/*@	lemma is_sorted_inductive_step{L} :
  @		\forall int* a, integer lb, ub, p;
  @			left_part_less{L}(a, p, lb, ub) && is_sorted(a, lb, p) && is_sorted(a, p, ub)
  @				==> is_sorted(a, lb, ub);
 */

///*@	lemma is_sorted_inductive_base{L} :
//  @		\forall int* a, integer lb, ub;
//  @			(ub - lb <= 1) && a[lb] <= a[ub]
//  @				==> is_sorted(a, lb, ub);
// */

///*@	lemma retain_sorted{L1,L2} :
//  @ 	\forall int*a, integer i, j, lb, ub, size;
//  @			(0 <= lb <= i <= j <= ub < size
//  @				&& is_sorted{L1}(a, lb, ub)
//  @				&& sameArray{L1,L2}(a, size, i, j)
//  @				&& is_sorted{L2}(a, i-1, j+1))
//  @					==> is_sorted{L2}(a, lb, ub);
// */

/*@	lemma same_array_saving{L1,L2} :
  @ 	\forall int*a, integer i, j, lb, ub, size;
  @			(0 <= lb <= i <= j <= ub < size &&
  @				sameArray{L1,L2}(a, size, i, j)
  @					==> sameArray{L1,L2}(a, size, lb, ub));
 */

/*@	lemma same_array_inductive{L1,L2,L3} :
  @ 	\forall int*a, integer i, j, size;
  @			(0 <= i <= j < size &&
  @				sameArray{L1,L2}(a, size, i, j) && sameArray{L2,L3}(a, size, i, j)
  @					==> sameArray{L1,L3}(a, size, i, j));
 */

/*@	lemma same_array_saving_overlap{L1,L2} :
  @ 	\forall int*a, integer lb, ub, i, j, size;
  @			(0 <= i <= j <= size-1 && (lb >= ub) &&
  @				sameArray{L1,L2}(a, size, lb, ub)
  @					==> sameArray{L1,L2}(a, size, i, j));
 */

/*@	lemma sorting_permut_left{L1,L2} :
  @ 	\forall int*a, integer lb, ub, p, size;
  @			(0 <= lb <= p <= ub <= size-1 &&
  @				left_part_less{L1}(a, p, lb, ub) &&
  @				permut{L1,L2}(a, size) && sameArray{L1,L2}(a, size, lb, p-1)
  @					==> left_part_less{L2}(a, p, lb, ub));
 */

/*@	lemma sorting_permut_right{L1,L2} :
  @ 	\forall int*a, integer lb, ub, p, size;
  @			(0 <= lb <= p <= ub <= size-1 &&
  @				left_part_less{L1}(a, p, lb, ub) &&
  @				permut{L1,L2}(a, size) && sameArray{L1,L2}(a, size, p+1, ub)
  @					==> left_part_less{L2}(a, p, lb, ub));
 */

/*@	lemma is_sorted_inductive_step{L} :
  @		\forall int* a, integer lb, ub, p;
  @			is_sorted(a, lb, p-1) && (left_part_less(a, p, lb, ub))
  @				==> is_sorted(a, lb, p);
 */

/*@	lemma is_sorted_from_sameArray{L1,L2} :
  @ 	\forall int*a, integer lb, i,j,size;
  @			(0 <= lb <= i <= j <= size-1 &&
  @				is_sorted{L1}(a, lb, i) &&
  @				sameArray{L1,L2}(a, size, i, j)
  @					==> is_sorted{L2}(a, lb, i));
 */

/*@ lemma is_sorted_empty{L1} :
 @		\forall int*a, integer ub, i,j;
  @			(0 <= j <= i <= ub ==>
  @				is_sorted{L1}(a, i, j));
 */

/*@	lemma is_sorted_from_sameArray_right{L1,L2} :
  @ 	\forall int*a, integer ub, i,j,size;
  @			(0 <= i <= j <= ub <= size-1 &&
  @				is_sorted{L1}(a, j+1, ub) &&
  @				sameArray{L1,L2}(a, size, i, j)
  @					==> is_sorted{L2}(a, j+1, ub));
 */

/*@	lemma left_part_less_from_sameArray{L1,L2} :
  @ 	\forall int*a, integer ub, lb, size;
  @			(0 <= lb <= ub <= size-1 &&
  @				left_part_less{L1}(a, ub+1, lb, size-1) &&
  @				sameArray{L1,L2}(a, size, lb, ub) && permut{L1,L2}(a, size)
  @					==> left_part_less{L2}(a, ub+1, lb, size-1));
 */

/*@	lemma left_part_less_from_sameArray_left{L1,L2} :
@ 	\forall int*a, integer ub, lb, p, j, size;
@			(0 <= j <= p <= lb <= ub <= size-1 &&
@				left_part_less{L1}(a, p, j, size-1) &&
@				sameArray{L1,L2}(a, size, lb, ub) && permut{L1,L2}(a, size)
@					==> left_part_less{L2}(a, p, j, size-1));
*/

/*@ lemma arifmetic_order{L} :
 @  \forall int* lbstack, integer i, pos;
 @			((\forall integer i; 1 <= i < pos
              ==> lbstack[i] < lbstack[i+1])
              	  ==> (\forall integer i; 1 <= i < pos
              	  	  ==> lbstack[i] < lbstack[pos]));
 */

/*@ lemma left_part_less_hole{L} :
@ 	(\forall int*a, integer lb1, ub1, lb2, ub2;
		is_sorted(a, ub1, lb2)
		&& left_part_less(a, ub1+1, lb1, lb2-1)
		&& left_part_less(a, lb2-1, ub1+1, ub2)
		==> left_part_less(a, ub1+1, lb1, ub2));
*/

//==>	is_sorted(a, ubstack[i], lbstack[i+1])
//	&& left_part_less(a, ubstack[i]+1, lbstack[i], lbstack[i+1]-1)
//	&& left_part_less(a, lbstack[i+1]-1, ubstack[i]+1, size-1))

/*@ lemma hole_sameArray{L1,L2} :
@ 	(\forall int*a, integer lb1, ub1, lb2, ub2, lb3, ub3, size;
@		(0 <= lb1 <= ub1 <= lb2 <= ub2 <= lb3 <= ub3 <= size-1 &&
@				is_sorted{L1}(a, ub1, lb2)
@				&& left_part_less{L1}(a, ub1+1, lb1, lb2-1)
@				&& left_part_less{L1}(a, lb2-1, ub1+1, ub2)
@				&& sameArray{L1,L2}(a, size, lb3, ub3))
@					==>
@					(is_sorted{L2}(a, ub1, lb2)
@					&& left_part_less{L2}(a, ub1+1, lb1, lb2-1)
@					&& left_part_less{L2}(a, lb2-1, ub1+1, ub2)));
*/

/*     !! @ lemma hole_sameArray_stack{L1,L2} :
@ 	(\forall int*a, int* lbstack, int* ubstack, integer pos, integer lb, integer ub, integer size;
@		(\forall integer i; 1 <= i < pos
@			==>	(0 <= lbstack[i] <= ubstack[i] <= lbstack[i+1] <= ubstack[i+1] <= lb <= ub <= size-1
@				&& is_sorted{L1}(a, ubstack[i], lbstack[i+1])
@				&& left_part_less{L1}(a, ubstack[i]+1, lbstack[i], lbstack[i+1]-1)
@				&& left_part_less{L1}(a, lbstack[i+1]-1, ubstack[i]+1, size-1)
@				&& sameArray{L1,L2}(a, size, lb, ub)))
@		==>
@		(\forall integer j; (1 <= j < pos
@			==>	(is_sorted{L2}(a, ubstack[j], lbstack[j+1])
@				&& left_part_less{L2}(a, ubstack[j]+1, lbstack[j], lbstack[j+1]-1)
@				&& left_part_less{L2}(a, lbstack[j+1]-1, ubstack[j]+1, size-1)))));
*/

/*@lemma hole_sameArray_stack{L1,L2} :
@ 	(\forall int*a, int* lbstack, int* ubstack, integer pos, integer lb, integer ub, integer size;
@		(\forall integer i; 1 <= i < pos
@			==>	((0 <= lbstack[i] <= ubstack[i] <= lbstack[i+1] <= ubstack[i+1] <= lb <= ub <= size-1)
@				&& good_hole{L1}(a, lbstack, ubstack, i, size)
@				&& sameArray{L1,L2}(a, size, lb, ub)))
@		==>
@		(\forall integer j; (1 <= j < pos
@			==>	good_hole{L2}(a, lbstack, ubstack, j, size))));
*/



//===functions===

/*@ requires (0 <= i <= j) && (j < size);
 @ 	requires \valid_range(a, 0, size-1);
 @	ensures
 @		(0 <= i < size) && (0 <= j < size)
 @		&&
 @		Swap{Old, Here}(a, size, i, j)
 @		&&
 @		sameArray{Pre,Here}(a, size, i, j);
 */
void swap (int *a, int size, int i, int j) {
  int v;
  v = a[i];
  a[i] = a[j];
  a[j] = v;
}


/*@
@	requires (0 <= lb < i) && (i < size)
@		&& (\forall integer k; lb+1 <= k <= i-1 ==> a[k] <= a[lb]);
@ 	requires \valid_range(a, 0, size-1);
@	ensures
@		i-1 <= \result <= i
@		&& (\forall integer k; lb <= k <= \result ==> a[k] <= a[\result])
@		&& (\forall integer res; res == \result ==>
@                          a[lb] == \old(a[res]) && a[res] == \old(a[lb]))
@		&& a[\result] <= a[i]
@ 		&&
@		permut{Pre,Here}(a, size)
@		&&
@		sameArray{Pre,Here}(a, size, lb, i)
@		;
*/
int mv_pv (int *a, int size, int lb, int i) {
	int res;
	if (a[i] < a[lb]) {
		swap(a, size, lb, i);
		res =  i;
	}
	else {
		swap(a, size, lb, i - 1);
		res = i - 1;

	}
	return res;
}


/*@	requires (0 <= lb < ub) && (ub < size);
@ 	requires \valid_range(a, 0, size-1);
@	ensures
@		(lb <= \result <= ub)
@		&&
@		high_bound (a, lb, \result,  a[\result])
@		&&
@		low_bound (a, \result, ub, a[\result])
@		&&
@		permut{Pre,Here}(a, size)
@		&&
@		sameArray{Pre,Here}(a, size, lb, ub);
*/
int partition (int* a, int size, int lb, int ub)
{
	int pivot, i, j, res;
	pivot = a[lb];
	i = lb + 1;
	j = ub;

	/*@	loop invariant
	 @		lb + 1 <= i <= ub
	 @		&&
	 @		j <= ub
	 @		&&
	 @ 		i <= j + 1
	 @		&&
	 @ 		high_bound (a, lb + 1, i-1, pivot)
	 @		&&
	 @		low_bound (a, j + 1, ub, pivot)
	 @		&&
	 @		permut{Pre,Here}(a, size)
	 @		&&
	 @		sameArray{Pre,Here}(a, size, lb, ub)
	 @		&&
	 @		a[lb] == pivot
	 @		;
	 @ 	loop variant
	 @		size - i + j;
	 */
	while (i < j)
	{
		//все элементы массива до a[i] меньше, чем pivot
		/*@	loop invariant
		 @ 		i <= j + 1
		 @		&&
		 @ 		high_bound (a, lb + 1, i-1, pivot)
		 @		&&
		 @		lb + 1 <= i <= ub
		 @		&&
	 	 @		sameArray{Pre,Here}(a, size, lb, ub)
		 @		;
		 @ 	loop variant
		 @		size - i;
		 */
		while (a[i] <= pivot && i < j) {
			i++;
		}

		//все элементы массива до a[j] больше, чем pivot
		/*@	loop invariant
		 @ 		low_bound (a, j+1, ub, pivot)
		 @		&&
		 @		j <= ub
		 @		&&
		 @		(a[i] > pivot || i >= j)
		 @		&&
		 @		i <= j + 1
		 @		&&
	 	 @		sameArray{Pre,Here}(a, size, lb, ub)
		 @		;
		 @ 	loop variant
		 @		j;
		 */
		while (a[j] >= pivot && i < j) {
			j--;
		}

		if ( i < j ) {

			/*@ ensures permut{Old,Here}(a, size)
			 @		&&
			 @		a[i] < pivot
			 @		&&
			 @		a[j] > pivot
			 @		&&
	 	 	 @		sameArray{Old,Here}(a, size, i, j);
			 */
			swap(a, size, i, j);
			i++;
			j--;
			/*@ assert
			 @		high_bound (a, lb + 1, i-1, pivot)
			 @		&&
			 @		low_bound (a, j + 1, ub, pivot);
			 */
		}
    }

	res = mv_pv (a, size, lb, i);

	return res;
}

///*@	requires 0 <= lb && ub < size;
// @ 	requires \valid_range(a, 0, size-1);
// @	decreases (ub - lb + 2);
// @	ensures
// @		is_sorted(a, lb, ub)
// @		&&
// @		permut{Pre,Here}(a, size)
// @		&&
// @		sameArray{Pre,Here}(a, size, lb, ub);
//*/
//
//void qSortRec (int *a, int size, int lb, int ub)
//{
//   int p;
//   if (lb < ub)
//     {
//       p = partition(a, size, lb, ub);
//       /*@assert
//        @	left_part_less(a, p, lb, ub);
//        */
//
//       qSortRec(a, size, lb, p-1);
//       XXX1:
//       /*@assert
//        @	sameArray{Pre,Here}(a, size, lb, ub);
//        */
//       /*@assert
//        @	left_part_less(a, p, lb, ub);
//        */
//       /*@assert
//        @	is_sorted(a, lb, p);
//        */
//       qSortRec(a, size, p+1, ub);
//       /*@assert
//        @	left_part_less(a, p, lb, ub);
//        */
//       /*@assert
//        @	is_sorted(a, p, ub);
//        */
//       /*@assert
//        @	is_sorted{XXX1}(a, lb, p);
//        */
//       /*@assert
//           @sameArray{XXX1,Here}(a, size, p, ub);
//       */
//       /*@assert
//        @	is_sorted(a, lb, p);
//        */
//     }
//}


/*@
 @ requires size > 0;
 @ requires \valid_range(a, 0, size-1);
 @ ensures is_sorted(a, 0, size-1);
 @ ensures permut{Pre,Here}(a, size);
 */
void qSortI(int a[], int size) {

       int p = 0;

       int lbstack[MAXSTACK], ubstack[MAXSTACK];       // стек запросов

       int pos = 1;       // текущая позиция стека

       int processedElems = size;

       if (size <= 1) {
               return;
       }

       int lb = 0;
       int ub = size - 1;
       int aux = 0;

       lbstack[1] = 0;
       ubstack[1] = size-1;

       lbstack[0] = 0;
       ubstack[0] = size-1;

       /*@loop invariant
@               pos >= 0
@               &&
@               (\forall integer i; 0 <= i <= pos ==> lbstack[i] >= 0)
@               &&
@               (\forall integer i; 0 <= i <= pos ==> ubstack[i] <= size - 1)
@               &&
@               permut{Pre,Here}(a, size)
@               &&
@               is_sorted(a, ubstack[ pos ] + 1, size-1)
				&&
				left_part_less(a, ubstack[pos]+1, lbstack[pos], size-1)
				&&
				(\forall integer i; 1 <= i < pos
					==>	good_hole(a, lbstack, ubstack, i, size))
				&&
				(\forall integer i; 1 <= i <= pos
					==> left_part_less(a, ubstack[i]+1, lbstack[i], size-1))
				&&
				(\forall integer i; 1 <= i <= pos
					==> lbstack[i] < ubstack[i])
				&&
				(\forall integer i; 1 <= i < pos
					==> ubstack[i] < lbstack[i+1])
@               ;
       */
       while ( pos > 0 ) {// пока есть запросы в стеке
               // Взять границы lb и ub текущего массива из стека.
           lb = lbstack[ pos ];
           ub = ubstack[ pos ];
           METKA1:

//   		is_sorted(a, ub1, lb2)
//   		&& left_part_less(a, ub1+1, lb1, lb2-1)
//   		&& left_part_less(a, lb2-1, ub1+1, ub2)
//   		==> left_part_less(a, ub1+1, lb1, ub2);

//           /*@ assert
//            	is_sorted(a, ub, lbstack[pos+1])
//				&& left_part_less(a, ub+1, lb, lbstack[pos+1]-1)
//				&& left_part_less(a, lbstack[pos+1]-1, ub+1, size-1);
//		   */

           /*@ assert
             (\forall integer i; 1 <= i < pos
					==>	good_hole{L1}(a, lbstack, ubstack, i, size));
            */


           /*@ assert (\forall integer i; 1 <= i < pos ==> lbstack[i] < lbstack[i+1]);*/
           /*@ assert (\forall integer i; 1 <= i < pos ==> lbstack[i] < lb);*/

           /*@ assert left_part_less(a, ub+1, lb, size-1); */
           /*@ assert is_sorted(a, ub+1, size-1); */

           /*@ assert (\forall integer i; 1 <= i <= pos
					==> left_part_less(a, ubstack[i]+1, lbstack[i], size-1));
					*/
           pos--;

             //if (lb < ub) { //it's always true for arrays longer 1 element
           /*@ assert lb < ub; */

                     p = partition(a, size, lb, ub);
                     /*@ assert left_part_less(a, p, lb, ub); */

                     /*@ assert lb >= 0 && p >= 0; */
                     /*@ assert ub < size && p-1 < size; */

                     /*@ assert is_sorted{METKA1}(a, ub+1, size-1)
                       @		&&
                       @		sameArray{METKA1,Here}(a, size, lb, ub);
                       */
                     /*@ assert is_sorted{Here}(a, ub+1, size-1); */

                     /*@assert
                       @  0 <= lb <= ub <= size-1 &&
                       @	left_part_less{METKA1}(a, ub+1, lb, size-1) &&
                       @	sameArray{METKA1,Here}(a, size, lb, ub) && permut{METKA1,Here}(a, size);
                     */

                     /*@ assert (\forall integer i; 1 <= i <= pos
                           ==> 0 <= lbstack[i] <= ubstack[i]+1 <= lb <= ub <= size-1 &&
								left_part_less{METKA1}(a, ubstack[i]+1, lbstack[i], size-1) &&
								sameArray{METKA1,Here}(a, size, lb, ub) && permut{METKA1,Here}(a, size));
								*/

                     /*@ assert left_part_less(a, ub+1, lb, size-1); */

                     /*@ assert (\forall integer i; 1 <= i <= pos
                             ==> left_part_less(a, ubstack[i]+1, lbstack[i], size-1)); */

//
//                     0 <= lb1 <= ub1 <= lb2 <= ub2 <= size-1 &&
//                     @				is_sorted{L1}(a, ub1, lb2)
//                     @				&& left_part_less{L1}(a, ub1+1, lb1, lb2-1)
//                     @				&& left_part_less{L1}(a, lb2-1, ub1+1, ub2)
//                     @				&& sameArray{L1,L2}(a, size, lb2, ub2))



                     /*@ assert
					 (\forall integer i; 1 <= i < pos
						==>	0 <= lbstack[i] <= ubstack[i] <= lbstack[i+1] <= ubstack[i+1] <= lb <= ub <= size-1
							&& good_hole{METKA1}(a, lbstack, ubstack, i, size)
							&& sameArray{METKA1,Here}(a, size, lb, ub));
					 */


					 /*@ assert
					 (\forall integer i; 1 <= i < pos
						==>	good_hole{L1}(a, lbstack, ubstack, i, size));
					 */


                     if (p+1 < ub) {
                    	 if (lb < p-1) {

							 pos++;
							 lbstack[ pos ] = lb;
							 ubstack[ pos ] = p-1;
							 /*@ assert (\forall integer i; 0 <= i <= pos ==> lbstack[i] >= 0); */
							 /*@ assert (\forall integer i; 0 <= i <= pos ==> ubstack[i] <= size - 1); */

							 /*@ assert
							 (\forall integer i; 1 <= i < pos
							 					==>	good_hole{L1}(a, lbstack, ubstack, i, size));
							 */


							 pos++;
							 /*@ assert (\forall integer i; 1 <= i < pos   ==> lbstack[i] < ubstack[i]); */
							 /*@ assert (\forall integer i; 1 <= i < pos-1 ==> ubstack[i] < lbstack[i+1]); */
							 lbstack[ pos ] = p+1;
							 /*@ assert (\forall integer i; 1 <= i < pos   ==> lbstack[i] < ubstack[i]); */
							 /*@ assert (\forall integer i; 1 <= i < pos-1 ==> ubstack[i] < lbstack[i+1]); */
							 ubstack[ pos ] = ub;
							 /*@ assert (\forall integer i; 1 <= i < pos  ==> lbstack[i] < ubstack[i]); */
							 /*@ assert (\forall integer i; 1 <= i <= pos ==> lbstack[i] < ubstack[i]); */

							 /*@ assert (\forall integer i; 1 <= i < pos-1 ==> ubstack[i] < lbstack[i+1]); */
							 /*@ assert (\forall integer i; 1 <= i < pos   ==> ubstack[i] < lbstack[i+1]); */

							 /*@ assert is_sorted(a, ub+1, size-1); */

							 /*@ assert
							 (\forall integer i; 1 <= i < pos
							 					==>	good_hole{L1}(a, lbstack, ubstack, i, size));
							 */

//							 /*@ assert left_part_less(a, ubstack[pos]+1, lbstack[pos], size-1); */
						 }
                    	 else {

							 pos++;
							 /*@ assert (\forall integer i; 1 <= i < pos   ==> lbstack[i] < ubstack[i]); */
							 /*@ assert (\forall integer i; 1 <= i < pos-1 ==> ubstack[i] < lbstack[i+1]); */
							 lbstack[ pos ] = p+1;
							 /*@ assert (\forall integer i; 1 <= i < pos   ==> lbstack[i] < ubstack[i]); */
							 /*@ assert (\forall integer i; 1 <= i < pos-1 ==> ubstack[i] < lbstack[i+1]); */
							 ubstack[ pos ] = ub;
							 /*@ assert (\forall integer i; 1 <= i < pos  ==> lbstack[i] < ubstack[i]); */
							 /*@ assert (\forall integer i; 1 <= i <= pos ==> lbstack[i] < ubstack[i]); */

							 /*@ assert (\forall integer i; 1 <= i < pos-1 ==> ubstack[i] < lbstack[i+1]); */
							 /*@ assert (\forall integer i; 1 <= i < pos   ==> ubstack[i] < lbstack[i+1]); */

							 /*@ assert is_sorted(a, ub+1, size-1); */

//							/*@ assert (\forall integer i; 1 <= i <= pos ==> left_part_less(a, ubstack[i]+1, lbstack[i], size-1)); */
                    	 }
                     }
                     else {
                    	 if (lb < p-1) {
							 pos++;
							 lbstack[ pos ] = lb;
							 ubstack[ pos ] = p-1;
							 /*@ assert (\forall integer i; 0 <= i <= pos ==> lbstack[i] >= 0); */
							 /*@ assert (\forall integer i; 0 <= i <= pos ==> ubstack[i] <= size - 1); */

						 }
						 else {
							 /* ub-1 <= p <= lb + 1 ; */
							 /*@ assert is_sorted(a, lb, ub); */
							 /*@ assert is_sorted(a, ub+1, size-1); */

							 /*@assert left_part_less(a, ub+1, lb, size-1); */

							 /*@assert is_sorted(a, lb, size-1); */
							 p = p;
						 }
                     }
             //}
             //else {
            // }

  }
       /*@     assert
         @             pos == 0;
       */
       /*@     assert
         @             (ubstack[pos] == 0)
         @             ||
         @             (ubstack[pos] == 1 && is_sorted(a, 0, 1) &&
left_part_less(a, 1, 0, size-1) && is_sorted(a, 1, size-1));
       */
}
//int main() {
//	int a[] = {1, 3, 3, 6, 2, 7};
//	qSortI(a, 6);
//}