Guest User

Untitled

a guest
Nov 12th, 2019
82
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. /*@
  2. predicate
  3. Sorted{L}(int* a, integer m, integer n) =
  4. \forall integer i, j; m <= i <= j < n ==> a[i] <= a[j];
  5. */
  6.  
  7. // lemma one: \forall integer x
  8. /*@ predicate GapSorted(int* a, integer m, integer n, integer gap) =
  9. @ \forall integer i, j; (m <= i <= j < n && j % gap == i % gap) ==> a[i] <=
  10. a[j];
  11. @
  12. */
  13.  
  14. /*@
  15. @ requires \valid(arr + (0..n-1));
  16. @ requires n > 1;
  17. @ ensures Sorted(arr, 0, n);
  18. */
  19. void shell_lr(int *arr, int n) {
  20. int i, j, tmp, gap;
  21. gap = n;
  22. /*@
  23. @ loop invariant 0 <= gap <= n/2;
  24. @ //loop invariant \forall integer k; (gap < k <= n/2) ==>GapSorted(arr, 0, n, k);
  25.  
  26. @ loop variant gap;
  27. */
  28. for (gap = n / 2; gap > 0; gap--) {
  29. /*@ loop invariant gap <= i <= n;
  30. @ loop invariant GapSorted(arr, 0, i, gap);
  31. @// loop invariant (gap == 1) ==> GapSorted(arr, 0, i, 1);
  32. @ loop variant n - i; */
  33. for (i = gap; i < n; ++i) {
  34. tmp = arr[i];
  35. /*
  36. @ loop invariant 0 <= j <= i;
  37. @ loop invariant arr[j] >= tmp;
  38. @ loop invariant j == i ==> GapSorted(arr, 0, i, gap);
  39. @ loop invariant j < i ==> GapSorted(arr, 0, i+1, gap);
  40. @ loop invariant \forall integer k; j <= k < i ==> arr[k] >= tmp;
  41. @ loop variant j;
  42. @*/
  43. for (j = i; j >= gap && arr[j - gap] > tmp; j -= gap) {
  44. arr[j] = arr[j - gap];
  45. //@ assert arr[j] >= arr[j - gap];
  46. //@ assert tmp < arr[j - gap];
  47. }
  48. arr[j] = tmp;
  49. // assert \forall integer l; j <= l <= i && l % gap == 0 ==> arr[j] <=
  50. // arr[l];
  51.  
  52. }
  53.  
  54. //@ assert gap > 0;
  55. //@ assert GapSorted(arr, 0, n, gap);
  56. }
  57. //@ assert (gap == 0) ==> GapSorted(arr, 0, i, 1);
  58. }
RAW Paste Data