• API
• FAQ
• Tools
• Archive
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.
Not a member of Pastebin yet?