Frama-C阶函数

Question

我试图用Frama和ACSL语言证明我的排序函数'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条款的合同。此外，在证明下，上述函数的所有循环都必须有一个loop assigns子句。如果不是这样，WP将得出结论，内存状态的任何部分都可能被调用(resp )修改。循环)，这样它就不能在相应的指令之后说出任何有意义的话。

因此，至少应将现有子句添加/替换为：

• 在swap合同中，assigns t[i], t[j];条款
• 在外部循环的循环注释中，一个子句loop assigns i, t[0 .. l-1];
• 在内环的循环注释中，一个子句loop assigns j, t[i .. l-1];

作为附带说明，关于loop assigns

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

请注意，您的注释可能存在其他问题，但这些是最明显的问题，在尝试证明更深层次的函数属性之前，拥有适当的assigns子句可能是最重要的。