SHARE
TWEET

Untitled

a guest Nov 12th, 2019 70 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
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!
 
Top