# 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