#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); //}