0

祝大家有美好的一天！我写了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);
    }
4

1 回答 1

0

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

  • 缺少关闭函数主体的大括号
  • 的ghost声明gap1不能与循环注释混合。这应该是两个不同的注释。无论如何，我没有看到使用gap1（尤其是因为它没有在循环内更新），一切都可以用gap. 如果您要实现的目标是为整个循环注释提供一个局部变量，那么这在 ACSL 中是不可能的：您有\let gap1 = ...; ...结构，但它的范围只是一个术语/谓词：您不能与 cross 共享它两个loop invariants（或loop invariants 和loop variant）

现在，您最紧迫的问题是loop assigns循环注释中缺少。您必须为所有循环提供此类子句，否则 WP 将无法对循环后的程序状态做出太多假设（例如，有关更多详细信息，请参见此答案）。您可能还想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两个内部循环的不变量，这可能需要更多的工作和比适合这种格式的答案更长的时间。

于 2019-12-20T13:56:39.390 回答