Существует программная реализация сортировки Shell в C, и я также аннотировал ее для проверки в Frama-C. Невозможно правильно составить инварианты и доказать правильность программы. Пожалуйста, помогите, если вы можете ...
/*@ predicate Sorted{L}(int *a, integer l, integer h) =
@ \forall integer i,j; l <= i <= j < h ==> a[i] <= a[j] ;
@*/
/*@ requires \valid_range(arr,0,n-1);
@ ensures Sorted(arr,0,n-1);
@*/
void shell(int *arr, int n) {
int i, j, tmp, gap;
/*@ loop invariant 0 <= i < n;
@ loop invariant Sorted(arr,0,i);
@*/
for (gap = n / 2; gap > 0; gap /= 2) {
/*@ loop invariant 0 <= i < n;
@ loop invariant Sorted(arr,0,i);
@*/
for (i = gap; i < n; ++i) {
tmp = arr[i];
/*@ loop invariant 0 <= j <= i < n;
@ loop invariant j == i ==> Sorted(arr,0,i);
@ loop invariant j < i ==> Sorted(arr,0,i+1);
@ loop invariant \forall integer k; j <= k < i ==> arr[k] > gap;
@ loop invariant \forall integer k; j <= k <= i ==> arr[k-gap] > tmp;
@ loop invariant j >= gap >0 && arr[j-gap] > tmp;
@ loop variant j;
@*/
for (j = i; j >= gap && arr[j - gap] > tmp; j -= gap) {
arr[j] = arr[j - gap];
}
arr[j] = tmp;
}
}
}