/*@
  predicate
    Sorted{L}(int* a, integer m, integer n) =
      \forall integer i, j; m <= i <= j < n ==> a[i] <= a[j];
*/

// lemma one: \forall integer x
/*@ predicate GapSorted(int* a, integer m, integer n, integer gap) =
  @   \forall integer i, j; (m <= i <= j < n && j % gap == i % gap) ==> a[i] <=
  a[j];
  @
 */

/*@
  @ requires \valid(arr + (0..n-1));
  @ requires n > 1;
  @ ensures Sorted(arr, 0, n);
  */
void shell_lr(int *arr, int n) {
  int i, j, tmp, gap;
  gap = n;
  /*@
    @ loop invariant 0 <= gap <= n/2;
    @ //loop invariant \forall integer k; (gap < k <= n/2) ==>GapSorted(arr, 0, n, k);

    @ loop variant gap;
  */
  for (gap = n / 2; gap > 0; gap--) {
    /*@ loop invariant gap <= i <= n;
       @ loop invariant GapSorted(arr, 0, i, gap);
       @// loop invariant (gap == 1) ==> GapSorted(arr, 0, i, 1);
       @ loop variant n - i; */
    for (i = gap; i < n; ++i) {
      tmp = arr[i];
      /*
        @ loop invariant 0 <= j <= i;
        @ loop invariant arr[j] >= tmp;
        @ loop invariant j == i ==> GapSorted(arr, 0, i, gap);
        @ loop invariant j < i ==> GapSorted(arr, 0, i+1, gap);
        @ loop invariant \forall integer k; j <= k < i ==> arr[k] >= tmp;
        @ loop variant j;
        @*/
      for (j = i; j >= gap && arr[j - gap] > tmp; j -= gap) {
        arr[j] = arr[j - gap];
        //@ assert arr[j] >= arr[j - gap];
        //@ assert tmp < arr[j - gap];
      }
      arr[j] = tmp;
      // assert \forall integer l; j <= l <= i && l % gap == 0 ==> arr[j] <=
      // arr[l];

    }

    //@ assert gap > 0;
    //@ assert GapSorted(arr, 0, n, gap);
  }
  //@ assert (gap == 0) ==> GapSorted(arr, 0, i, 1);
}