验证Shell Sorting算法循环不变量？

Question

大家好！写了Shell排序验证码，但是无法构建正确的循环不变量，无法正确组合不变量，证明程序的正确性……请帮帮我！

/*@ predicate Sorted{L}(int* a, integer m, integer n) =
  @ \forall integer i, j; m <= i <= j < n ==> a[i] <= a[j];
*/
/*@ 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 GapSorted(arr, 0, n, 1);
*/
void shell_lr(int *arr, int n) {
int i, j, tmp, gap;
/*@ ghost int gap1 = n
  @ loop invariant 0 <= gap1 <= n/2;
  @ loop invariant gap1 < n/2 ==> GapSorted(arr, 0, n, gap+1);
  @ //loop invariant \forall integer k; gap < k <= n/2 ==> GapSorted(arr, 0, n, k);
  @ loop variant gap1;
*/
for (gap = n / 2; gap > 0; gap--) {
    /*@ loop invariant 0 <= i <= n;
       @ //loop invariant \forall integer m; gap < m <= n/2 ==> GapSorted(arr, 0, i, m);
       @ loop invariant GapSorted(arr, 0, i, gap);
       @ 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 \forall integer k; (j < k <= i) ==> GapSorted(arr, 0, i, k);
          @// loop invariant \forall integer k; j <= k <= gap ==> GapSorted(arr, k, i,               gap);
          @ 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];
        }
        //@ assert j>=0;
        arr[j] = tmp;
    }
    //@ assert i == n;
    //@ assert GapSorted(arr, 0, i, gap);
    //@ assert gap > 0;
    // assert GapSorted(arr, 0, n, gap);
    }

Answer 1

首先，您提供的代码在语法上不正确：

• 缺少关闭函数主体的大括号
• gap1 的 ghost 声明不能与循环注释混合。这应该是两个不同的注释。反正我看不到gap1的用法（特别是因为它没有在循环内更新），一切都可以用gap来表达。如果您想要实现的是为整个循环注释设置一个局部变量，那么这在 ACSL 中是不可能的：您有 \let gap1 = ...; ... 构造，但它的范围只是一个术语/谓词：您不能共享它跨越两个loop invariants（或loop invariants 和loop variant）

现在，您最紧迫的问题是循环注释中缺少loop assigns。您必须为所有循环提供此类子句，否则 WP 将无法对循环后的程序状态做出太多假设（例如，请参阅 this answer 了解更多详细信息）。您可能还想在中间循环中将i 上的不变量加强一点为gap <= i <= n，但这是一个细节。

通过以下循环分配，您的大部分注释都得到了证明（Frama-C 20.0 Calcium with -wp -wp-rte）。

/*@ predicate Sorted{L}(int* a, integer m, integer n) =
  @ \forall integer i, j; m <= i <= j < n ==> a[i] <= a[j];
*/
/*@ 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 GapSorted(arr, 0, n, 1);
*/
void shell_lr(int *arr, int n) {
int i, j, tmp, gap;
/*@
  @ loop invariant 0 <= gap <= n/2;
  @ loop invariant gap < n/2 ==> GapSorted(arr, 0, n, gap+1);
  @ loop assigns gap, i, j, tmp, arr[0 .. n - 1];
  @ //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 \forall integer m; gap < m <= n/2 ==> GapSorted(arr, 0, i, m);
       @ loop invariant GapSorted(arr, 0, i, gap);
       loop assigns i,j,tmp,arr[0..n-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 \forall integer k; (j < k <= i) ==> GapSorted(arr, 0, i, k);
          @// loop invariant \forall integer k; j <= k <= gap ==> GapSorted(arr, k, i,               gap);
            loop assigns j, arr[gap .. i];
          @ 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];
        }
        //@ assert j>=0;
        arr[j] = tmp;
    }
    //@ assert i == n;
    //@ assert GapSorted(arr, 0, i, gap);
    //@ assert gap > 0;
    // assert GapSorted(arr, 0, n, gap);
    }
}

还有待证明的是两个内部循环的 GapSorted 不变量，这可能需要更多的工作和比适合这种格式的答案更长的时间。