c - Frama-C 排序函数

Question

我正在尝试使用 ACSL 语言用 Frama-C 证明我的排序函数“order”的正确性。我有一个额外的“交换”函数来置换数组“t”的两个值。

编辑:我更新了我的代码。

/*@ 
    requires \valid (t+ (0..(l-1)));
    requires l > 0;
    requires i<l && j<l && i>=0 && j>=0;
    assigns t[i], t[j];
    ensures t[j] == \old(t[i]);
    ensures t[i] == \old(t[j]);
*/
void swap(int *t, int l, int i,int j){
  int tmp;
  tmp = t[i];
  t[i] = t[j];
  t[j] = tmp;
  return;
}

/*@ 
    requires \valid (t+ (0..(l-1)));
    requires l > 0;
    ensures \forall integer k; (0 <= k < l-1) ==> t[k] <= t[k+1]; 
*/
void order(int *t, int l) {
  int i;
  int j;
/*@
    loop assigns i, t[0 .. l-1];
    loop invariant 0<=i<l && i>=0;
    loop invariant \forall integer k; (0 <= k<=i) ==> t[k] <= t[k+1]; 
    loop variant l-i;


*/
  for (i=0;i<l;i++) {

/*@
    loop assigns j, t[0 .. l-1];
    loop invariant i<=j<l && i>=0 && j>=0;
    loop invariant  \forall  integer k; (0 <= k <= j)  ==> (t[k] <=  t[k+1]);
    loop variant l-j;

*/
    for (j=i; j<l; j++) {

      if (t[i] > t[j]){
    /*@ assert t[i] > t[j] && i<l && j<l && i>=0 && j>=0 ; */
    swap(t, l, i, j);
    /*@ assert t[i] < t[j] && i<l && j<l && i>=0 && j>=0 ; */
      }
    }
  }
}

感谢您的帮助!

Answer 1

与往常一样，在使用 WP 时，证明函数调用的所有函数都配备带有 assigns 子句的契约(Contract)是至关重要的。此外，证明中所述函数的所有循环都必须有一个 loop assigns 子句。如果不是这种情况，WP 将得出结论，内存状态的任何部分都可能被调用(相应的循环)修改，因此它无法在相应的指令之后说出任何有意义的内容。

因此，至少，您应该通过以下方式添加/替换现有子句:

• 在swap的合约中，一个子句assigns t[i], t[j];
• 在外层循环的循环注解中，一个子句loop assigns i, t[0 .. l-1];
• 在内循环的循环注解中，一个子句loop assigns j, t[i .. l-1];

关于循环分配的旁注:

• 它们必须描述从第一次进入循环到当前步骤的所有潜在修改(因此 t[i], t[j] 是不够的，因为可能还有其他在当前 j 之前发生的交换)。
• 循环的索引(此处为i 和j)必须是循环赋值的一部分，尽管很容易忽略它并想知道为什么 WP 不是快乐。

请注意，您的注释可能还有其他问题，但这些是最明显的问题，并且拥有适当的 assigns 子句可能是尝试证明更深层次的功能属性之前最重要的事情.