diff --git a/block_quicksort/block_partition_hoare_finish.c b/block_quicksort/block_partition_hoare_finish.c new file mode 100644 index 0000000..5c8cb95 --- /dev/null +++ b/block_quicksort/block_partition_hoare_finish.c @@ -0,0 +1,115 @@ +#define BLOCKSIZE 3 + +static inline int block_partition_hoare_finish(int *arr, int begin, int end) +{ + int last = end - 1; + int mid = begin + ((end - begin) / 2); + unsigned char indexL[BLOCKSIZE], indexR[BLOCKSIZE]; + if (less(arr[mid], arr[begin])) + { + if (less(arr[last], arr[begin])) + { + if (less(arr[mid], arr[last])) + { + swap(arr[begin], arr[last]); + } + else + { + int temp = arr[mid]; + arr[mid] = arr[last]; + arr[last] = arr[begin]; + arr[begin] = arr[temp]; + } + } + } + else + { // mid > begin + if (less(arr[last], arr[begin])) + { // mid > begin > last + swap(arr[mid], arr[last]); + } + else + { + if (arr[mid] < arr[last]) + { // begin < mid < last + swap(arr[begin], arr[mid]); + } + else + { // begin < mid, mid > last + int temp = arr[mid]; + arr[mid] = arr[begin]; + arr[begin] = arr[last]; + arr[last] = temp; + } + } + } + + int q = arr[begin]; + mid = begin++; + int temp; + last--; + int iL = 0; + int iR = 0; + int sL = 0; + int sR = 0; + int j; + int num; + while (last - begin + 1 > 2 * BLOCKSIZE) + { + if (iL == 0) + { + sL = 0; + for (j = 0; j < BLOCKSIZE; j++) + { + indexL[iL] = j; + iL += !(arr[begin + j] < q); + } + } + if (iR == 0) + { + sR = 0; + for (j = 0; j < BLOCKSIZE; j++) + { + indexR[iR] = j; + iR += !(q < arr[last - j]); + } + } + num = min(iL, iR); + if (num != 0) + { + temp = arr[begin + indexL[sL]]; + arr[begin + indexL[sL]] = arr[last - indexR[sR]]; + for (j = 1; j < num; j++) + { + arr[last - indexR[sR + j - 1]] = arr[begin + indexL[sL + j]]; + arr[begin + indexL[sL + j]] = arr[last - indexR[sR + j]]; + } + arr[last - indexR[sR + num - 1]] = temp; + } + iL -= num; + iR -= num; + sL += num; + sR += num; + if (iL == 0) + begin += BLOCKSIZE; + if (iR == 0) + last -= BLOCKSIZE; + } + begin--; + last++; +loop: + do + ; + while (arr[++begin] < q); + do + ; + while (q < arr[--last]); + if (begin <= last) + { + swap(arr[begin], arr[last]); + goto loop; + } + swap(arr[mid], arr[last]); + return last; +} + diff --git a/block_quicksort/block_quicksort b/block_quicksort/block_quicksort new file mode 100755 index 0000000..6aadd82 Binary files /dev/null and b/block_quicksort/block_quicksort differ diff --git a/block_quicksort/block_quicksort.c b/block_quicksort/block_quicksort.c new file mode 100644 index 0000000..9dd93d9 --- /dev/null +++ b/block_quicksort/block_quicksort.c @@ -0,0 +1,440 @@ +#include +#include +#include + +#define BLOCKSIZE 2 +/*@ predicate sorted(int* tab, integer first, integer last) = + \forall integer x,y; first <= x <= y < last ==> tab[x] <= tab[y]; +*/ + +/*@ predicate swap{L1, L2}(int *a, int *b, integer begin, integer i, integer j, integer end) = + begin <= i < end && begin <= j < end && + \at(a[i], L1) == \at(b[j], L2) && + \at(a[j], L1) == \at(b[i], L2) && + \forall integer k; begin <= k < end && k != i && k != j ==> \at(a[k], L1) == \at(b[k], L2); +*/ + +/*@ predicate same_array{L1,L2}(int *a, int *b, integer begin, integer end) = + \forall integer k; begin <= k < end ==> \at(a[k],L1) == \at(b[k],L2); +*/ + +/*@ predicate partitioned(int *a, integer begin, integer end, integer pivot) = + (\forall integer k; begin <= k < pivot ==> a[k] <= a[pivot]) && + (\forall integer l; pivot < l < end ==> a[pivot] < a[l]); +*/ + +// When all elements are leq than value at L1, they have to be leq than value at L2 +/*@ predicate preserve_upper_bound{L1,L2}(int *a, integer begin, integer end, integer value) = + (∀ int p; begin <= p < end ==> \at(a[p],L1) <= value) ==> + (∀ int p; begin <= p < end ==> \at(a[p],L2) <= value); +*/ + +/*@ predicate preserve_all_upper_bounds{L1,L2}(int *a, integer begin, integer end) = + (\forall integer v; preserve_upper_bound{L1,L2}(a, begin, end, v)); +*/ + +// When all elements are bigger than value at L1, they have to be bigger than value at L2 +/*@ predicate preserve_lower_bound{L1,L2}(int *a, integer begin, integer end, integer value) = + (∀ int p; begin <= p < end ==> \at(a[p],L1) > value) ==> + (∀ int p; begin <= p < end ==> \at(a[p],L2) > value); +*/ + +/*@ predicate preserve_all_lower_bounds{L1,L2}(int *a, integer begin, integer end) = + (\forall integer v; preserve_lower_bound{L1,L2}(a, begin, end, v)); +*/ + +/*@ inductive same_elements{L1, L2}(int *a, int *b, integer begin, integer end) { + case refl{L1, L2}: + \forall int *a, int *b, integer begin, end; + same_array{L1,L2}(a, b, begin, end) ==> + same_elements{L1, L2}(a, b, begin, end); + case swap{L1, L2}: \forall int *a, int *b, integer begin, i, j, end; + swap{L1, L2}(a, b, begin, i, j, end) ==> + same_elements{L1, L2}(a, b, begin, end); + case trans{L1, L2, L3}: \forall int* a, int *b, int *c, integer begin, end; + same_elements{L1, L2}(a, b, begin, end) ==> + same_elements{L2, L3}(b, c, begin, end) ==> + same_elements{L1, L3}(a, c, begin, end); +}*/ + +/*@ + @ logic integer count_elt{L1}(int *a, integer l, integer u, int v) = + @ (l == u) ? 0 + @ : (((v == \at(a[l], L1)) ? 1 : 0) + count_elt{L1}(a, l + 1, u, v)); + @*/ + +// valid hier entfernen, das macht man nicht in predicates +/*@ + @ predicate permutation{L1, L2}(int *a, int *b, int l, int u) = + @ \forall int v; count_elt{L1}(a, l, u, v) == count_elt{L2}(b, l, u, v); + @*/ + +int min(int a, int b) +{ + return (a < b ? a : b); +} + +/*@ + @ requires + @ \valid(array + i) + @ ∧ \valid(array + j); + requires \valid(array + (0 .. upper-1)); + requires i >=0 && i< upper; + requires j >=0 && j< upper; + terminates \true; + @ assigns + @ array[i], array[j]; + @ ensures + @ array[i] == \old(array[j]) + @ ∧ array[j] == \old(array[i]); + @ ensures same_elements{Pre, Post}( array, array, (int)0, upper); + ensures swap{Pre, Post}(array, array, (int)0, i,j, upper); + @*/ +void swap(int *array, int i, int j, + /* ghost: */ int upper) +{ + int tmp = array[i]; + array[i] = array[j]; + array[j] = tmp; +} +/*@ + @ requires + @ 0 <= l < l + 1 < u < INT_MAX; + @ requires + @ \valid(array + (l .. u - 1)); + terminates \true; + @ assigns + @ \nothing; + @ ensures + @ l <= \result < u; + @*/ +int choose_pivot(int *array, int l, int u) +{ + return l + ((u - l) / 2); +} +/*@ + @ requires + @ 0 <= l < l + 1 < u < INT_MAX; + requires u <= upper; + @ requires + @ \valid(array + (0 .. upper - 1)); + terminates \true; + @ assigns + @ *(array + (l .. u - 1)); + @ ensures + @ l <= \result < u; + @ ensures + @ partitioned(array, l, u, \result); + @ ensures + @ ∀ int v; preserve_upper_bound{Pre,Post}(array, l, u, v); + @ ensures + @ ∀ int v; preserve_lower_bound{Pre,Post}(array, l, u, v); + @ + @ ensures same_elements{Pre, Post}( array, array, 0, upper); + @*/ +int block_partition(int *array, int l, int u, + /* ghost: */ int upper) +{ + int block_l[BLOCKSIZE] = {0}; + int block_r[BLOCKSIZE] = {0}; + int i = l; + int j = u - 1; + int m = choose_pivot(array, l, u); + printf("pivot: %i\n", m); + + int num_left = 0; // elements in block + int num_right = 0; + + int start_left = 0; + int start_right = 0; + +preswap1: + swap(array, j, m, + /*ghost: */ upper); + m = j; + print_array(array, upper); + printf("pivot value: %i\n", array[m]); + //@ assert same_elements{Pre, Here}(array, array, 0, upper); + /*@ + @ loop invariant + @ l < i <= j < u; + @ loop invariant + @ (∀ int p; l < p < i ==> array[p] <= array[l]) + @ && (∀ int q; j < q < u ==> array[l] < array[q]); + @ loop invariant + @ ∀ int v; preserve_upper_bound{Pre,Here}(array, l, u, v); + @ loop invariant + @ ∀ int v; preserve_lower_bound{Pre,Here}(array, l, u, v); + @ loop invariant + @ same_elements{Pre, Here}(array, array, 0, upper); + @ loop assigns + @ i, j, *(array + (l .. u - 1)); + @ loop variant j-i; + @*/ + + while (j - i + 1 > 2 * BLOCKSIZE) + { + printf("main loop. num_left: %i, num_right: %i, start_left: %i, start_right: %i\n", num_left, num_right, start_left, start_right); + + CurrentOuter: + + //@ assert ∀ int p; l < p < i ==> array[p] <= array[l]; + /*@ + @ loop invariant + @ l + 1 <= i <= j < u; + @ loop invariant + @ ∀ int q; j < q <= \at(j, CurrentOuter) ==> + @ array[l] < array[q]; + @ loop assigns + @ j; + @ loop variant j-i; + @*/ + if (num_left == 0) + { // only fill blocks when they are empty + + start_left = 0; + for (int a = 0; a < BLOCKSIZE; a++) + { + if (array[a + i] >= (array[m])) + { + printf("store %i in block_l[%i]\n", a + 1, num_left); + // store in block + block_l[num_left] = a; + num_left++; + } + } + } + + if (num_right == 0) + { // only fill blocks when they are empty + + start_right = 0; + for (int a = 0; a < BLOCKSIZE; a++) + { + if (array[j - a] <= (array[m])) + { + printf("store %i in block_r[%i]\n", j - a, num_right); + // store in block + block_r[num_right] = a; + num_right++; + } + } + } + // rearange + int num_min = min(num_left, num_right); + printf("num_min: %i\n", num_min); + + for (int a = 0; a < num_min; a++) + { + swap(array, i + block_l[start_left + a], j - block_r[start_right + a], upper); + } + num_left -= num_min; + num_right -= num_min; + start_left += num_min; + start_right += num_min; + i += (num_left == 0) ? BLOCKSIZE : 0; + j -= (num_right == 0) ? BLOCKSIZE : 0; + // end rearrange + } + + // end main loop + // now the gap between l and u is smaller than 2*BLOCKSIZE + + int shiftR = 0; + int shiftL = 0; + + if (num_right == 0 && num_left == 0) + { + shiftL = ((j - i) + 1) / 2; + shiftR = (j - i) + 1 - shiftL; + // midpoint or midpoints (even length) + assert(shiftL >= 0); + assert(shiftL <= BLOCKSIZE); + assert(shiftR >= 0); + assert(shiftR <= BLOCKSIZE); + + start_left = 0; + start_right = 0; + + for (int a = 0; a < shiftL; a++) + { + if (array[a + i] >= (array[m])) + { + // store in block + block_l[num_left] = a; + num_left++; + } + if (array[j - a] <= (array[m])) + { + // store in block + block_r[num_right] = a; + num_right++; + } + } + + if (shiftL < shiftR) + { + assert(shiftL + 1 == shiftR); + if (array[j - shiftR] <= (array[m])) + { + // store in block + block_r[num_right] = shiftR - 1; + num_right++; + } + } + } + else if (num_right != 0) + { + shiftL = (j - i) - BLOCKSIZE + 1; + shiftR = BLOCKSIZE; + assert(shiftL >= 0); + assert(shiftL <= BLOCKSIZE); + assert(num_left == 0); + + start_left = 0; + for (int a = 0; a < shiftL; j++) + { + if (array[a + i] >= (array[m])) + { + // store in block + block_l[num_left] = a; + num_left++; + } + } + } + else + { + shiftL = BLOCKSIZE; + shiftR = (j - i) - BLOCKSIZE + 1; + assert(shiftR >= 0); + assert(shiftR <= BLOCKSIZE); + assert(num_right == 0); + start_right = 0; + for (int a = 0; a < shiftR; a++) + { + if (array[j - shiftR] <= (array[m])) + { + // store in block + block_r[num_right] = a; + num_right++; + } + } + } + + // rearange final + int num_min = min(num_left, num_right); + + for (int a = 0; a < num_min; a++) + { + swap(array, l + block_l[start_left + a], u - block_r[start_right + a], upper); + } + num_left -= num_min; + num_right -= num_min; + start_left += num_min; + start_right += num_min; + i += (num_left == 0) ? shiftL : 0; + j -= (num_right == 0) ? shiftR : 0; + // end rearrange final + + // one of the two buffers might still contain elements + + if (num_left != 0) + { + + assert(num_right == 0); + int lowerI = start_left + num_left - 1; + int up = j - i; + + while (lowerI >= start_left && block_l[lowerI] == up) + { + upper--; + lowerI--; + } + while (lowerI >= start_left) + swap(array, i + up--, i + block_l[lowerI--], upper); + swap(array, m, i + up + 1, upper); + return i + up + 1; + } + else if (num_right != 0) + + { + assert(num_left == 0); + int lowerI = start_right + num_right - 1; + int up = j - i; + + while (lowerI >= start_right && block_r[lowerI] == up) + { + + upper--; + lowerI--; + } + while (lowerI >= start_left) + swap(array, j - up--, j - block_r[lowerI--], upper); + + swap(array, m, j - up, upper); + return j - up; + } + else + { + // no remaining elements + + assert(j + 1 == i); + swap(array, m, i, upper); + return i; + } +} + +/*@ + @ requires + @ 0 <= first <= last < INT_MAX; + @ requires + @ \valid(t + (0 .. upper - 1)); + requires last <= upper; + @ assigns + @ *(t + (first .. last - 1)); + @ ensures + @ \forall int v; preserve_upper_bound{Pre, Post}(t, first, last, v); + @ ensures + @ \forall int v; preserve_lower_bound{Pre, Post}(t, first, last, v); + @ ensures + @ sorted(t, first, last); + @ ensures + @ same_elements{Pre, Post}(t, t, 0, upper); + @*/ +void sort(int *t, int first, int last, + /* ghost: */ int upper) +{ + if (last - first <= 1) + { + return; + } + //@ assert 1 < last-first; + //@ assert same_elements{Pre, Here}(t, t, 0, upper); + + int pivot = block_partition(t, first, last, + /* ghost: */ upper); + //@ assert same_elements{Pre, Here}(t, t, 0, upper); +part: + sort(t, first, pivot, + /* ghost: */ upper); + //@ assert same_elements{part, Here}(t, t, 0, upper); + //@ assert same_elements{Pre, Here}(t, t, 0, upper); + //@ assert \forall int v; preserve_upper_bound{Pre, Here}(t, first, last, v); + //@ assert \forall int v; preserve_lower_bound{Pre, Here}(t, first, last, v); + //@ assert preserve_lower_bound{part, Here}(t, pivot + 1, last, t[pivot]); + sort(t, pivot + 1, last, + /* ghost: */ upper); + //@ assert same_elements{Pre, Here}(t, t, 0, upper); + //@ assert preserve_upper_bound{part, Here}(t, first, pivot, t[pivot]); + //@ assert preserve_lower_bound{part, Here}(t, pivot + 1, last, t[pivot]); +} + +void print_array(int *arr, int len) +{ + for (int j = 0; j < len; j++) + { + printf("%d ", arr[j]); + } + printf("\n"); +} + diff --git a/block_quicksort/block_quicksort_original b/block_quicksort/block_quicksort_original new file mode 100755 index 0000000..47baefc Binary files /dev/null and b/block_quicksort/block_quicksort_original differ diff --git a/block_quicksort/block_quicksort_original.c b/block_quicksort/block_quicksort_original.c new file mode 100644 index 0000000..b2bffb1 --- /dev/null +++ b/block_quicksort/block_quicksort_original.c @@ -0,0 +1,561 @@ + +#include +#include +#include +#include + +/*@ predicate sorted(int* tab, integer first, integer last) = + \forall integer x,y; first <= x <= y < last ==> tab[x] <= tab[y]; +*/ + +/*@ predicate swap{L1, L2}(int *a, int *b, integer begin, integer i, integer j, integer end) = + begin <= i < end && begin <= j < end && + \at(a[i], L1) == \at(b[j], L2) && + \at(a[j], L1) == \at(b[i], L2) && + \forall integer k; begin <= k < end && k != i && k != j ==> \at(a[k], L1) == \at(b[k], L2); +*/ + +/*@ predicate same_array{L1,L2}(int *a, int *b, integer begin, integer end) = + \forall integer k; begin <= k < end ==> \at(a[k],L1) == \at(b[k],L2); +*/ + +/*@ predicate partitioned(int *a, integer begin, integer end, integer pivot) = + (\forall integer k; begin <= k < pivot ==> a[k] <= a[pivot]) && + (\forall integer l; pivot < l < end ==> a[pivot] < a[l]); +*/ + +// When all elements are leq than value at L1, they have to be leq than value at L2 +/*@ predicate preserve_upper_bound{L1,L2}(int *a, integer begin, integer end, integer value) = + (∀ int p; begin <= p < end ==> \at(a[p],L1) <= value) ==> + (∀ int p; begin <= p < end ==> \at(a[p],L2) <= value); +*/ + +/*@ predicate preserve_all_upper_bounds{L1,L2}(int *a, integer begin, integer end) = + (\forall integer v; preserve_upper_bound{L1,L2}(a, begin, end, v)); +*/ + +// When all elements are bigger than value at L1, they have to be bigger than value at L2 +/*@ predicate preserve_lower_bound{L1,L2}(int *a, integer begin, integer end, integer value) = + (∀ int p; begin <= p < end ==> \at(a[p],L1) > value) ==> + (∀ int p; begin <= p < end ==> \at(a[p],L2) > value); +*/ + +/*@ predicate preserve_all_lower_bounds{L1,L2}(int *a, integer begin, integer end) = + (\forall integer v; preserve_lower_bound{L1,L2}(a, begin, end, v)); +*/ + +/*@ inductive same_elements{L1, L2}(int *a, int *b, integer begin, integer end) { + case refl{L1, L2}: + \forall int *a, int *b, integer begin, end; + same_array{L1,L2}(a, b, begin, end) ==> + same_elements{L1, L2}(a, b, begin, end); + case swap{L1, L2}: \forall int *a, int *b, integer begin, i, j, end; + swap{L1, L2}(a, b, begin, i, j, end) ==> + same_elements{L1, L2}(a, b, begin, end); + case trans{L1, L2, L3}: \forall int* a, int *b, int *c, integer begin, end; + same_elements{L1, L2}(a, b, begin, end) ==> + same_elements{L2, L3}(b, c, begin, end) ==> + same_elements{L1, L3}(a, c, begin, end); +}*/ + +/*@ + + predicate array_lower_bound{L1}(int* arr, int n, int x, int begin, int *z, int q) = +(\forall int v; 0 <= v < \at(x,L1) ==> \at(arr[begin+\at(z[v], L1)], L1) > q); + + predicate array_upper_bound{L1}(int* arr, int n, int x, int last, int *z, int q) = +(\forall int v; 0 <= v < \at(x,L1) ==> \at(arr[last-\at(z[v], L1)], L1) <= q); + +lemma array_lower_bound_next{L1, L2}: +\forall int *arr, n, x, begin, *z, q; +(\at(x, L1) != \at(x, L2) ==> array_lower_bound{L1}(arr, n, x, begin, z, q)) && +(\at(x, L1) != \at(x, L2) ==> same_array{L1, L2}(arr, arr, 0, n)) && +(\at(x, L1) != \at(x, L2) ==> same_array{L1, L2}(z, z, 0, \at(x, L1))) && +(\at(x, L1) != \at(x, L2) ==> \at(x, L1) + 1 == \at(x, L2)) && +(\at(x, L1) != \at(x, L2) ==> \at(arr[begin+\at(z[x-1], L2)], L2) > q) ==> +(\at(x, L1) != \at(x, L2) ==> array_lower_bound{L2}(arr, n, x, begin, z, q)); +*/ + +/*@ + + predicate all_in_block_are_bigger(int* arr, int n, int x, int begin, int *z, int q) = + \forall int v; 0 <= v < x ==> arr[begin + z[v]] > q; + + predicate all_in_block_are_lower(int* arr, int n, int x, int last, int *z, int q) = + \forall int v; 0 <= v < x ==> arr[last - z[v]] <= q; + +*/ +// /*@ + +// lemma same_array_implication{L1, L2}: +// \forall int q, *arr, n, x, y; +// same_array{L1,L2}(arr, arr, 0, n) && +// array_upper_bound{L1}(arr, n, x, y, q) ==> +// array_upper_bound{L2}(arr, n, x, y, q); + +// */ + +/*@ + +lemma swap_compare{L1,L2}: +\forall int *arr, upper, x, y, q; +0<= x +\at(arr[x],L1) <= q && +swap{L1,L2}(arr, arr, 0, x, y, upper) ==> +\at(arr[y], L2) <= q; + + +*/ +/*@ + + requires i >=0 && i< upper; + requires j >=0 && j< upper; + @ assigns + @ array[i], array[j]; + @ ensures + @ array[i] == \old(array[j]) + @ ∧ array[j] == \old(array[i]); + @ ensures same_elements{Pre, Post}( array, array, (int)0, upper); + ensures swap{Pre, Post}(array, array, (int)0, i,j, upper); + @*/ +void swap(int *array, int i, int j, + /* ghost: */ int upper) +{ + int tmp = array[i]; + array[i] = array[j]; + array[j] = tmp; +} + +/*@ +ensures a <=b ==> \result == a; +ensures a >= b ==> \result == b; +ensures \result <= a; +ensures \result <= b; +assigns \nothing; + + +*/ +int min(int a, int b) +{ + return (a < b ? a : b); +} + +/*@ + @ requires + @ 0 q; + */ + while (end - begin + 1 > 2 * 3) + { + end++; + } + return 1; +} +/*@ + @ requires + @ 0 <= l < l + 1 < u < INT_MAX; + requires u <= upper; + terminates \true; + @ assigns + @ *(array + (l .. u - 1)); + @ ensures + @ l <= \result < u; + @ ensures + @ partitioned(array, l, u, \result); + @ ensures + @ \forall int v; preserve_upper_bound{Pre,Post}(array, l, u, v); + @ ensures + @ \forall int v; preserve_lower_bound{Pre,Post}(array, l, u, v); + @ + @ ensures same_elements{Pre, Post}( array, array, 0, upper); + @*/ +int partition_pivot(int *array, int l, int u, int pivot_value, + /* ghost: */ int upper) +{ + int i = l; + int j = u - 1; +preswap1: + + //@ assert same_elements{Pre, Here}(array, array, 0, upper); + /*@ + @ loop invariant + @ l < i <= j < u; + @ loop invariant + @ (\forall int p; l < p < i ==> array[p] <= pivot_value) + @ && (\forall int q; j < q < u ==> pivot_value < array[q]); + @ loop invariant + @ \forall int v; preserve_upper_bound{Pre,Here}(array, l, u, v); + @ loop invariant + @ \forall int v; preserve_lower_bound{Pre,Here}(array, l, u, v); + @ loop invariant + @ same_elements{Pre, Here}(array, array, 0, upper); + @ loop assigns + @ i, j, *(array + (l+1 .. u - 1)); + @ loop variant j-i; + @*/ + while (i < j) + { + scan1: + /*@ + @ loop invariant + @ l < i <= j < u; + @ loop invariant + @ \forall int p; \at(i, scan1) <= p < i ==> + @ array[p] <= pivot_value; + @ loop assigns + @ i; + @ loop variant j-i; + @*/ + while (i < j && array[i] <= pivot_value) + { + i += 1; + } + scan2: + //@ assert \forall int p; l < p < i ==> array[p] <= pivot_value; + /*@ + @ loop invariant + @ l < i <= j < u; + @ loop invariant + @ \forall int q; j < q <= \at(j, scan2) ==> + @ pivot_value < array[q]; + @ loop assigns + @ j; + @ loop variant j-i; + @*/ + while (i < j && pivot_value < array[j]) + { + j -= 1; + } + //@ assert \forall int q; j < q < u ==> pivot_value < array[q]; + if (i < j) + { + //@ assert array[i] > pivot_value >= array[j]; + swap(array, i, j, + /*ghost: */ upper); + //@ assert array[i] <= pivot_value < array[j]; + } + } // End of outer loop + if (array[i] > pivot_value) + { + i -= 1; + } + + return i; +} +/*@ + @ requires + @ 0 <= begin < begin + 1 < end ; + requires begin <= pivot_position < end; + + @ assigns + @ *(arr + (begin .. end - 1)); + @ ensures + @ begin <= \result < end; + @ ensures + @ partitioned(arr, begin, end, \result); + @ ensures + @ ∀ int v; preserve_upper_bound{Pre,Post}(arr, begin, end, v); + @ ensures + @ ∀ int v; preserve_lower_bound{Pre,Post}(arr, begin, end, v); + @*/ +int block_partition_hoare_finish(int *arr, int begin, int end, int pivot_position, /* ghost: */ int upper) +{ + // print_array(arr + begin, end - begin); + int last = end - 1; + + swap(arr, pivot_position, begin, upper); + //@ assert same_elements{Pre, Here}(arr, arr, 0, upper); + int pivot_location = begin; + int q = arr[pivot_location]; + begin++; + // printf("block_partition: "); + + // printf("pivot: %i\n", q); + int temp; + int iL = 0; + int iR = 0; + int sL = 0; + int sR = 0; + int j; + int num; + + int indexL1[3] = {0}, indexR1[3] = {0}; + int *indexL = indexL1; + int *indexR = indexR1; + // //@ assert \separated(arr+(0..upper-1), indexL+(0..3)); + /*@ + loop invariant same_elements{Pre, Here}(arr, arr, 0, upper); + + loop invariant indexL_bounds: \forall int v; 0<=v<3 ==> 0<=indexL[v]<3; + loop invariant indexR_bounds: \forall int v; 0<=v<3 ==> 0<=indexR[v]<3; + + loop invariant \forall int v; \at(begin, Pre) <= v < begin ==> arr[v] <= q; //0-begin are smaller + loop invariant \forall int v; last <= v < end ==> arr[v] > q; //last-end are bigger + + loop invariant all_that_existL: \forall int v; 0 <= v < 3 ==> ((\exists int i; 0<=i indexL[i] == v) ==> arr[begin+v] > q); + loop invariant all_that_dont_existL: \forall int v; 0 <= v < 3 ==> ((!\exists int i; 0<=i indexL[i] == v) ==> arr[begin+v] <= q); + loop invariant all_that_existR: \forall int v; 0 <= v < 3 ==> ((\exists int i; 0<=i indexR[i] == v) ==> arr[last-v] <= q); + loop invariant all_that_dont_existR: \forall int v; 0 <= v < 3 ==> ((!\exists int i; 0<=i indexR[i] == v) ==> arr[last-v] > q); + */ + while (last - begin + 1 > 2 * 3) + { + // //print_array(arr, upper); + + //@ assert begin + 3-1 arr[v] <= q; //0-begin are smaller + + loop invariant indexL_unchanged: same_array{LoopCurrent, Here}(indexL, indexL, 0, iL-1); + + //bounds on the contents of indexL + loop invariant indexL_bounds: \forall int v; 0<=v<3 ==> 0<=indexL[v]<3; + + loop invariant all_that_exist: \forall int v; 0 <= v < 3 ==> ((\exists int i; 0<=i indexL[i] == v) ==> arr[begin+v] > q); + loop invariant all_that_dont_exist: \forall int v; 0 <= v < 3 ==> ((!\exists int i; 0<=i indexL[i] == v) ==> arr[begin+v] <= q); + + loop invariant array_lower_bound(arr, upper, iL, begin, indexL, q); + loop assigns indexL[0..3-1]; + loop assigns iL, j; + */ + for (j = 0; j < 3; j++) + { + + //@ assert same_array{LoopCurrent, Here}(arr, arr, 0, upper); + //@ assert 0<= iL <3; + indexL[iL] = j; + + // bounds on the members of indexL + //@ assert 0<=indexL[iL]<3; + // @ assert array_upper_bound(arr, upper, iL, begin, indexL, q); + iL += !(arr[begin + j] <= q); + + //@ assert \at(iL, LoopCurrent) != iL ==> arr[begin + j] > q && \at(iL, LoopCurrent) +1 == iL; + + //@ assert \separated(arr+(0..upper-1), indexL+(0..3)); + + // force lemma + //@ assert (\at(iL, LoopCurrent) != \at(iL, Here) ==> array_lower_bound{LoopCurrent}(arr, upper, iL, begin, indexL, q)); + //@ assert (\at(iL, LoopCurrent) != \at(iL, Here) ==> same_array{LoopCurrent, Here}(arr, arr, 0, upper)); + //@ assert (\at(iL, LoopCurrent) != \at(iL, Here) ==> same_array{LoopCurrent, Here}(indexL, indexL, 0, \at(iL, LoopCurrent))); + //@ assert (\at(iL, LoopCurrent) != \at(iL, Here) ==> \at(iL, LoopCurrent) + 1 == \at(iL, Here)); + //@ assert (\at(iL, LoopCurrent) != \at(iL, Here) ==> \at(arr[begin+\at(indexL[iL-1], Here)], Here) > q); + + //@ assert \at(iL, LoopCurrent) != iL ==> array_lower_bound(arr, upper, iL, begin, indexL, q); + + //@ assert \at(iL, LoopCurrent) == iL ==> arr[begin + j] <= q; + //@ assert array_lower_bound(arr, upper, iL, begin, indexL, q); + } + } + if (iR == 0) + { + sR = 0; + /*@ + loop invariant 0<= j <= 3; + loop invariant 0 <= iR <= j; + loop invariant \forall int v; last <= v < end ==> arr[v] > q; //last-end are bigger + + loop invariant indexL_unchanged: same_array{LoopCurrent, Here}(indexR, indexR, 0, iR-1); + + //bounds on the contents of indexR + loop invariant indexR_bounds: \forall int v; 0<=v<3 ==> 0<=indexR[v]<3; + + loop invariant all_that_exist: \forall int v; 0 <= v < 3 ==> ((\exists int i; 0<=i indexR[i] == v) ==> arr[last-v] <= q); + loop invariant all_that_dont_exist: \forall int v; 0 <= v < 3 ==> ((!\exists int i; 0<=i indexR[i] == v) ==> arr[last-v] > q); + + loop invariant array_lower_bound(arr, upper, iR, last, indexR, q); + loop assigns indexR[0..3-1]; + loop assigns iR, j; + */ + for (j = 0; j < 3; j++) + { + //@ assert same_array{LoopCurrent, Here}(arr, arr, 0, upper); + //@ assert 0<= iR <3; + indexR[iR] = j; + + // bounds on the members of indexR + //@ assert 0<=indexR[iR]<3; + // @ assert array_lower_bound(arr, upper, iR, last, indexR, q); + iR += !(q < arr[last - j]); + + //@ assert \at(iR, LoopCurrent) != iR ==> arr[last - j] > q && \at(iR, LoopCurrent) +1 == iR; + + // //@ assert \separated(arr+(0..upper-1), indexR+(0..3-1)); + + // force lemma + //@ assert array_lower_bound{LoopCurrent}(arr, upper, iR, last, indexR, q); + //@ assert same_array{LoopCurrent, Here}(arr, arr, 0, upper); + //@ assert same_array{LoopCurrent, Here}(indexR, indexR, 0, \at(iR, LoopCurrent)); + //@ assert \at(iR, LoopCurrent) != iR ==> \at(iR, LoopCurrent) + 1 == \at(iR, Here); + //@ assert \at(iR, LoopCurrent) != iR ==> \at(arr[last-\at(indexL[iR-1], Here)], Here) > q ; + + //@ assert \at(iR, LoopCurrent) != iR ==> array_lower_bound(arr, upper, iR, last, indexL, q); + + //@ assert \at(iR, LoopCurrent) == iR ==> arr[last - j] > q; + //@ assert array_lower_bound(arr, upper, iL, last, indexR, q); + } + } + + num = min(iL, iR); + if (num != 0) + { + + //@ assert array_upper_bound(arr, upper, num, begin, indexL, q); + //@ assert array_lower_bound(arr, upper, num, last, indexR, q); + + /*@ + + loop invariant lower: \forall int v; 0 <= v < j ==> arr[begin+indexL[sL+v]] > q; + loop invariant upper: \forall int v; 0 <= v < j ==> arr[last-indexR[sR+v]] <= q; + + loop invariant lower: \forall int v; j <= v < num ==> arr[begin+indexL[sL+v]] <= q; + loop invariant upper: \forall int v; 0 <= v < num ==> arr[last-indexR[sR+v]] > q; + + loop assigns arr[begin..last]; + +*/ + for (j = 0; j < num; j++) + { + int x = begin + indexL[sL + j]; + int y = last - indexR[sR + j]; + + // //@ assert \separated(arr+(0..upper-1), indexR+(0..3-1)); + // //@ assert \separated(arr+(0..upper-1), indexL+(0..3-1)); + //@ assert arr[x] > q; + //@ assert arr[y] <= q; + preswap: + swap(arr, x, y, upper); + //@ assert arr[x] <= q; + //@ assert arr[begin + indexL[sL + j]] <= q; + //@ assert arr[y] > q; + //@ assert arr[last - indexR[sR + j]] > q; + } + // printf("swapping result: "); + // print_array(arr, end); + } + iL -= num; + iR -= num; + sL += num; + sR += num; + if (iL == 0) + begin += 3; + if (iR == 0) + last -= 3; + //@ assert same_elements{Pre, Here}(arr, arr, 0, upper); + } // end main loop + last++; + int mid = partition_pivot(arr, begin, last, q, upper); + swap(arr, pivot_location, mid, upper); + //@ assert same_elements{Pre, Here}(arr, arr, 0, upper); + + return mid; +} + +/*@ + @ requires + @ 0 <= l < l + 1 < u < INT_MAX; + + @ assigns + @ \nothing; + @ ensures + @ l <= \result < u; + @*/ +int choose_pivot(int *array, int l, int u) +{ + return l + ((u - l) / 2); +} + +/*@ + @ requires + @ 0 <= first <= last < INT_MAX; + + requires last <= upper; + @ assigns + @ *(t + (first .. last - 1)); + @ ensures + @ \forall int v; preserve_upper_bound{Pre, Post}(t, first, last, v); + @ ensures + @ \forall int v; preserve_lower_bound{Pre, Post}(t, first, last, v); + @ ensures + @ sorted(t, first, last); + @ ensures + @ same_elements{Pre, Post}(t, t, 0, upper); + @*/ +void sort(int *t, int first, int last, int upper) +{ + if (last - first <= 1) + { + return; + } + + //@ assert 1 < last-first; + //@ assert same_elements{Pre, Here}(t, t, 0, upper); + // sleep(1); + int pivot = block_partition_hoare_finish(t, first, last, choose_pivot(t, first, last), last); + //@ assert same_elements{Pre, Here}(t, t, 0, upper); +part: + // printf("leftsort(arr,%i,%i,%i)", first, pivot, upper); + sort(t, first, pivot, upper); + //@ assert same_elements{part, Here}(t, t, 0, upper); + //@ assert same_elements{Pre, Here}(t, t, 0, upper); + //@ assert \forall int v; preserve_upper_bound{Pre, Here}(t, first, last, v); + //@ assert \forall int v; preserve_lower_bound{Pre, Here}(t, first, last, v); + //@ assert preserve_lower_bound{part, Here}(t, pivot + 1, last, t[pivot]); + // printf("rightsort(arr,%i,%i,%i)", pivot + 1, last, upper); + sort(t, pivot + 1, last, upper); + //@ assert same_elements{Pre, Here}(t, t, 0, upper); + //@ assert preserve_upper_bound{part, Here}(t, first, pivot, t[pivot]); + //@ assert preserve_lower_bound{part, Here}(t, pivot + 1, last, t[pivot]); +} diff --git a/heapsort/heap.c b/heapsort/heap.c new file mode 100644 index 0000000..d85447c --- /dev/null +++ b/heapsort/heap.c @@ -0,0 +1,366 @@ +#include "Heap.acsl" +#include "MultisetOperations.acsl" +#include "MultisetRetainRest.acsl" +#include "MultisetParity.acsl" +#include "MultisetUpdate.acsl" +#include "IncreasingLemmas.acsl" +#include "ArrayBounds.acsl" +#include "WeaklyIncreasingLemmas.acsl" +#include "../../typedefs.h" + +/*@ + assigns \nothing; + ensures parent: \result == HeapParent(child); + */ +size_type +heap_parent(size_type child) +{ + return (0u < child) ? (child - 1u) / 2u : 0u; +} + +/*@ + requires bounds: 0 <= p < n; + requires valid: \valid(a + (0..n-1)); + assigns \nothing; + ensures bounds: p < \result <= n; + ensures parent: \result < n ==> p == HeapParent(\result); + ensures parent: \result < n-1 ==> HeapLeft(p) < n-1; + ensures parent: \result < n-1 ==> HeapRight(p) < n; + ensures left: HeapLeft(p) < n ==> \result < n; + ensures right: HeapRight(p) < n ==> \result < n; + ensures max: HeapLeft(p) < n ==> a[HeapLeft(p)] <= a[\result]; + ensures max: HeapRight(p) < n ==> a[HeapRight(p)] <= a[\result]; + ensures none: \result == n ==> n <= HeapLeft(p); + ensures none: \result == n ==> n <= HeapRight(p); +*/ +size_type +heap_child(const value_type *a, size_type n, size_type p) +{ + if (p + 1u <= n - p - 1u) { + const size_type left = 2u * p + 1u; + const size_type right = left + 1u; + + if (right < n) { + // case of two children: select child with maximum value + return a[right] <= a[left] ? left : right; + } + else { + // at most one child that comes before n-1 can exist + return left; + } + } + else { + return n; + } +} + +/*@ + requires valid: \valid_read(a + (0..n-1)); + assigns \nothing; + ensures bound: 0 <= \result <= n; + ensures heap: Heap(a, \result); + ensures last: \forall integer i; \result < i <= n ==> !Heap(a, i); +*/ +size_type +is_heap_until(const value_type *a, size_type n) +{ + size_type parent = 0u; + + /*@ + loop invariant bound: 0 <= parent < child <= n+1; + loop invariant parent: parent == HeapParent(child); + loop invariant heap: Heap(a, child); + loop invariant not_heap: a[parent] < a[child] ==> \forall integer i; child < i <= n ==> !Heap(a, i); + + loop assigns child, parent; + loop variant n - child; + */ + for (size_type child = 1u; child < n; ++child) { + if (a[parent] < a[child]) { + return child; + } + + if ((child % 2u) == 0u) { + // right child + ++parent; + } + } + + return n; +} + +/*@ + requires valid: \valid_read(a +(0..n-1)); + assigns \nothing; + ensures heap: \result <==> Heap(a, n); +*/ +bool +is_heap(const value_type *a, size_type n) +{ + return is_heap_until(a, n) == n; +} +/*@ + requires nonempty: 0 < n; + requires valid: \valid(a + (0..n-1)); + requires heap: Heap(a, n-1); + requires n2 >= n; + assigns a[0..n-1]; + ensures heap: Heap(a, n); + ensures MultisetReorder{Pre, Post}(a, n2); +*/ +void +push_heap(value_type *a, size_type n) /*@ ghost(size_type n2) */ // Everything is a heap, except for the very last element +{ + if (n <= 1) { + return; + } + + size_type child = n - 1; // element to be pushed in + size_type parent = heap_parent(child); + + // Check if parent is smaller than child + + if (a[child] > a[parent]) { + + // Swap the parent element down but store the child element in temp + value_type temp = a[child]; + a[child] = a[parent]; + + //@ assert Heap(a, n); + + // only one spot in the array was updated + //@ assert ArrayUpdate{Pre, Here}(a, n, child, a[parent]); + + // If temp would be at a[parent], the multiset would be unchanged + //@ assert MultisetParity{Pre, Here}(a, n, a[parent], temp); + + // Shift all the smaller ancestors down until we find the perfect spot for temp + + child = parent; + parent = heap_parent(child); + + /*@ + loop invariant 0<= child =1; + requires Heap(a, n); + + ensures Heap(a, n-1); + ensures MultisetReorder{Old,Here}(a, n); + + ensures a[n-1] == \old(a[0]); + ensures MaxElement(a, n, n-1); + + +*/ +void +pop_head(value_type *a, size_type n) // Move the head to the back and fix the heap 0..n-1 + +{ + if (n == 1 || a[n - 1] == a[0]) { + return; + } + + size_type parent = 0u; + size_type child = heap_child(a, n - 1u, parent); // biggest child + size_type temp = a[n - 1u]; + + // swap head with tail + + a[n - 1u] = a[parent]; + + //@ assert ArrayUpdate{Pre,Here}(a, n, n-1, a[parent]); + + // if a[p] was temp, the multiset would be equal + + //@ assert Heap(a, n-1); + + while (temp < a[child] && child < n - 1u) { + // while the perfect spot was not found and the end of the array was not reached + + // pull the child up + a[parent] = a[child]; + //@ assert ArrayUpdate{LoopCurrent,Here}(a, n, parent, a[child]) || Unchanged{LoopCurrent, Here}(a, 0, n); + //@ assert MultisetUpdate{LoopCurrent, Here}(a, n, parent, a[child]) || Unchanged{LoopCurrent, Here}(a, 0, n); + + // if a[child] was temp, the multiset would be unchanged + + // + + parent = child; + child = heap_child(a, n - 1u, parent); + } + + // the +} + +/*@ + requires \valid(a + (0..n-1)); + ensures Heap(a, n); + ensures MultisetReorder{Pre,Post}(a, n); + ensures Unchanged{Pre, Post}(a, n, n2); + assigns a[0..n-1]; + +*/ +void +heapify(value_type *a, size_type n) /*@ ghost(size_type n2) */ + +{ + if (n <= 1) { + return; + } + + /*@ + loop invariant Heap(a, i); + loop invariant MultisetReorder{Pre,Here}(a, n); + loop assigns a[0..n-1], i; + loop invariant Unchanged{Pre, Here}(a, i + 1, n); + + loop invariant 1 <=i<=n; + + */ + for (size_type i = 1u; i < n; i++) { + push_heap(a, i + 1u) /*@ ghost(n) */; + } +} +/*@ + requires \valid(a+(0..n-1)); +requires n>0; +assigns a[0..n-1]; +ensures MultisetReorder{Pre, Post}(a, n); +ensures Increasing(a, n); + +*/ +void +sort(value_type *a, size_type n) +{ + if (n == 1) { + return; + } + + heapify(a, n) /*@ ghost(n) */; + + /*@ + loop invariant 0u 1; i--) { + + if (a[0] == a[i - 1]) { + + //@ assert Heap(a, i-1); + //@ assert UpperBound(a, i, a[i-1]); + //@ assert MultisetReorder{Pre, Here}(a, n); + //@ assert LowerBound(a, i-1, n, a[i-1]); + continue; + } + + //@ assert Heap(a, i); + //@ assert MaxElement(a, i, 0); + value_type temp = a[0]; + + a[0] = a[i - 1u]; + //@ assert ArrayUpdate{LoopCurrent, Here}(a, n, 0, a[i-1]); + //@ assert MultisetUpdate{LoopCurrent, Here}(a, n, 0, a[i-1]); + + //@ assert MultisetParity{LoopCurrent, Here}(a, n, a[i-1u],temp); + + //@ assert Unchanged{LoopCurrent, Here}(a, i, n); + + //@ ghost L: ; + //@ assert a[i-1] != temp; + a[i - 1u] = temp; + + //@ assert ArrayUpdate{L, Here}(a, n, i-1, temp) ; + //@ assert MultisetUpdate{L, Here}(a, n, i-1, temp); + + //@ assert MultisetReorder{LoopCurrent, Here}(a, n); + //@ assert Unchanged{LoopCurrent, Here}(a, i, n); + //@ assert MaxElement(a, i, i-1); + + heapify(a, i - 1u) /*@ ghost(n) */; + //@ assert Heap(a, i-1); + //@ assert MaxElement(a, i, i-1); + //@ assert MultisetReorder{Pre, Here}(a, n); + //@ assert LowerBound(a, i-1, n, a[i-1]); + } + + //@ assert Increasing(a, n); +} diff --git a/quicksort/quicksort.c b/quicksort/quicksort.c index 1bb3cbc..bba6496 100644 --- a/quicksort/quicksort.c +++ b/quicksort/quicksort.c @@ -1,30 +1,251 @@ -void swap(int* x, int* y){ - int t = *x; - * x = *y; - *y = t; +#include +#include + +/*@ predicate sorted(int* tab, integer first, integer last) = + \forall integer x,y; first <= x <= y < last ==> tab[x] <= tab[y]; +*/ + +/*@ predicate swap{L1, L2}(int *a, int *b, integer begin, integer i, integer j, integer end) = + begin <= i < end && begin <= j < end && + \at(a[i], L1) == \at(b[j], L2) && + \at(a[j], L1) == \at(b[i], L2) && + \forall integer k; begin <= k < end && k != i && k != j ==> \at(a[k], L1) == \at(b[k], L2); +*/ + +/*@ predicate same_array{L1,L2}(int *a, int *b, integer begin, integer end) = + \forall integer k; begin <= k < end ==> \at(a[k],L1) == \at(b[k],L2); +*/ + +/*@ predicate partitioned(int *a, integer begin, integer end, integer pivot) = + (\forall integer k; begin <= k < pivot ==> a[k] <= a[pivot]) && + (\forall integer l; pivot < l < end ==> a[pivot] < a[l]); +*/ + +// When all elements are leq than value at L1, they have to be leq than value at L2 +/*@ predicate preserve_upper_bound{L1,L2}(int *a, integer begin, integer end, integer value) = + (\forall int p; begin <= p < end ==> \at(a[p],L1) <= value) ==> + (\forall int p; begin <= p < end ==> \at(a[p],L2) <= value); +*/ + +/*@ predicate preserve_all_upper_bounds{L1,L2}(int *a, integer begin, integer end) = + (\forall integer v; preserve_upper_bound{L1,L2}(a, begin, end, v)); +*/ + +// When all elements are bigger than value at L1, they have to be bigger than value at L2 +/*@ predicate preserve_lower_bound{L1,L2}(int *a, integer begin, integer end, integer value) = + (\forall int p; begin <= p < end ==> \at(a[p],L1) > value) ==> + (\forall int p; begin <= p < end ==> \at(a[p],L2) > value); +*/ + +/*@ predicate preserve_all_lower_bounds{L1,L2}(int *a, integer begin, integer end) = + (\forall integer v; preserve_lower_bound{L1,L2}(a, begin, end, v)); +*/ + +/*@ inductive same_elements{L1, L2}(int *a, int *b, integer begin, integer end) { + case refl{L1, L2}: + \forall int *a, int *b, integer begin, end; + same_array{L1,L2}(a, b, begin, end) ==> + same_elements{L1, L2}(a, b, begin, end); + case swap{L1, L2}: \forall int *a, int *b, integer begin, i, j, end; + swap{L1, L2}(a, b, begin, i, j, end) ==> + same_elements{L1, L2}(a, b, begin, end); + case trans{L1, L2, L3}: \forall int* a, int *b, int *c, integer begin, end; + same_elements{L1, L2}(a, b, begin, end) ==> + same_elements{L2, L3}(b, c, begin, end) ==> + same_elements{L1, L3}(a, c, begin, end); +}*/ + + +/*@ + @ requires + @ \valid(array + i) + @ ∧ \valid(array + j); + requires \valid(array + (0 .. upper-1)); + requires i >=0 && i< upper; + requires j >=0 && j< upper; + terminates \true; + @ assigns + @ array[i], array[j]; + @ ensures + @ array[i] == \old(array[j]) + @ ∧ array[j] == \old(array[i]); + @ ensures same_elements{Pre, Post}( array, array, (int)0, upper); + ensures swap{Pre, Post}(array, array, (int)0, i,j, upper); + @*/ +void swap(int *array, int i, int j, + /* ghost: */ int upper) +{ + int tmp = array[i]; + array[i] = array[j]; + array[j] = tmp; +} +/*@ + requires + 0 <= l < l + 1 < u; + requires + \valid(array + (l .. u - 1)); + terminates \true; + assigns + \nothing; + ensures + l <= \result < u; + */ +int choose_pivot(int *array, int l, int u) +{ + return l + ((u - l) / 2); } +/*@ + @ requires + 0 <= l < l + 1 < u; + requires u <= upper; + requires + \valid(array + (0 .. upper - 1)); + terminates \true; + assigns + *(array + (l .. u - 1)); + ensures \forall int v; preserve_upper_bound{Pre,Post}(array, l, u, v); + ensures + \forall int v; preserve_lower_bound{Pre,Post}(array, l, u, v); + ensures + l <= \result < u; + ensures + partitioned(array, l, u, \result); + -int partitionner(int* t, int premier, int dernier, int pivot){ - swap(t+pivot,t+dernier); - int j = premier; - for(int i = premier; i < dernier; i++){ - if(t[i] <=t[dernier]){ - swap(t+i,t+j); - j++; + + ensures same_elements{Pre, Post}( array, array, 0, upper); + */ +int partition(int *array, int l, int u, + /* ghost: */ int upper) +{ + int i = l + 1; + int j = u - 1; + int m = choose_pivot(array, l, u); +preswap1: + swap(array, l, m, + /*ghost: */ upper); + //@ assert same_elements{Pre, Here}(array, array, 0, upper); + /*@ + loop invariant + l < i <= j < u; + loop invariant + (\forall int p; l < p < i ==> array[p] <= array[l]) + && (\forall int q; j < q < u ==> array[l] < array[q]); + loop invariant + \forall int v; preserve_upper_bound{Pre,Here}(array, l, u, v); + loop invariant + \forall int v; preserve_lower_bound{Pre,Here}(array, l, u, v); + loop invariant + same_elements{Pre, Here}(array, array, 0, upper); + loop assigns + i, j, *(array + (l .. u - 1)); + loop variant j-i; + */ + while (i < j) + { + scan1: + /* + loop invariant + l < i <= j < u; + loop invariant + \forall int p; \at(i, scan1) <= p < i ==> + array[p] <= array[l]; + loop assigns + i; + loop variant j-i; + */ + while (i < j && array[i] <= array[l]) + { + i += 1; + } + scan2: + //@ assert \forall int p; l < p < i ==> array[p] <= array[l]; + /*@ + loop invariant + l < i <= j < u; + loop invariant + \forall int q; j < q <= \at(j, scan2) ==> + array[l] < array[q]; + loop assigns + j; + loop variant j-i; + */ + while (i < j && array[l] < array[j]) + { + j -= 1; + } + //@ assert \forall int q; j < q < u ==> array[l] < array[q]; + if (i < j) + { + //@ assert array[i] > array[l] >= array[j]; + swap(array, i, j, + /*ghost: */ upper); + //@ assert array[i] <= array[l] < array[j]; } } - swap(t+dernier,t+j); - return j; + if (array[l] < array[i]) + { + i -= 1; + } + swap(array, l, i, + /*ghost: */ upper); + return i; } -int choix_pivot(int* t, int premier, int dernier); //retunr a pivot between premier and dernier - -void tri_rapide(int* t, int premier, int dernier){ - if (premier < dernier){ - int pivot = choix_pivot(t, premier, dernier); - pivot = partitionner(t, premier, dernier, pivot); - tri_rapide(t, premier, pivot-1); - tri_rapide(t,pivot+1, dernier); +/*@ + requires + 0 <= first <= last < INT_MAX; + requires + \valid(t + (0 .. upper - 1)); + requires last <= upper; + assigns + *(t + (first .. last - 1)); + ensures + \forall int v; preserve_upper_bound{Pre, Post}(t, first, last, v); + ensures + \forall int v; preserve_lower_bound{Pre, Post}(t, first, last, v); + ensures + sorted(t, first, last); + ensures + same_elements{Pre, Post}(t, t, 0, upper); + */ +void sort(int *t, int first, int last, +/* ghost: */ int upper) +{ + if (last - first <= 1) + { + return; } - return; + //@ assert 1 < last-first; + //@ assert same_elements{Pre, Here}(t, t, 0, upper); + + int pivot = partition(t, first, last, + /* ghost: */ upper); + //@ assert same_elements{Pre, Here}(t, t, 0, upper); +part: + sort(t, first, pivot, + /* ghost: */ upper); + //@ assert same_elements{part, Here}(t, t, 0, upper); + //@ assert same_elements{Pre, Here}(t, t, 0, upper); + //@ assert \forall int v; preserve_upper_bound{Pre, Here}(t, first, last, v); + //@ assert \forall int v; preserve_lower_bound{Pre, Here}(t, first, last, v); + //@ assert preserve_lower_bound{part, Here}(t, pivot + 1, last, t[pivot]); + sort(t, pivot + 1, last, + /* ghost: */ upper); + //@ assert same_elements{Pre, Here}(t, t, 0, upper); + //@ assert preserve_upper_bound{part, Here}(t, first, pivot, t[pivot]); + //@ assert preserve_lower_bound{part, Here}(t, pivot + 1, last, t[pivot]); +} + + +void main() { + +int num[5] = {1, 4, 5, 7, 0}; + + +sort(num, 0, 5, 5); + + for(int j = 0; j < 5; j++) { + printf("%d ", num[j]); + } }