Frama-C无法验证assign子句求助：函数合约证明失败排查

我来帮你分析下为什么Frama-C的WP插件没法证明这个循环的assign子句，其实问题出在循环不变量的逻辑精度上，咱们一步步拆解：

问题根源 #

你的循环不变量 test: \forall int j; (n>j>i ==> a[j]==0); 只覆盖了大于当前i的数组元素，但每次循环修改的是a[i]——这个位置并不在当前不变量的覆盖范围内。WP需要明确知道每次循环修改的元素在操作后满足的状态，否则无法验证assign子句的正确性。

另外，原assign子句a[0..n-1]虽然整体上描述了循环最终修改的范围，但缺乏每次循环的精准修改信息，也会给WP的证明带来阻碍。

修改方案 #

调整循环不变量和assign子句，让逻辑更精准：

/*@ 
@ requires n>0; 
@ requires \valid(a+(0..n-1)); 
@ ensures \forall int i; (0 <= i < n ==> a[i]==0); 
@*/ 
void f(int n, float *a) { 
/*@ 
@ loop invariant \forall int j; (i < j < n ==> a[j] == 0);
@ loop invariant i >= -1; // 明确循环变量i的下界，循环结束后i=-1
@ loop assigns i, a[i]; // 精准声明每次循环只修改a[i]和i
@*/ 
for (int i=n-1; i>=0; i--) { 
    a[i] = 0; 
} 
}

为什么这样修改有效 #

1. 精准的assign子句：a[i]明确告诉WP，每次循环只会修改当前i对应的数组元素，避免了宽泛范围带来的证明模糊性。
2. 完善的循环不变量：
   • 第一个不变量保证了所有大于i的元素已经被置0，初始时i=n-1，没有元素满足i<j<n，不变量成立；每次循环i减1，刚被置0的a[i]会进入下一轮循环的j>i范围，不变量得以维护。
   • 第二个不变量i >= -1明确了i的合法范围，循环结束后i=-1，此时第一个不变量覆盖了0<=j<n的所有元素，正好匹配函数的ensures条件。

这样调整后，WP就能顺利完成assign子句以及所有合约的证明了。

内容的提问来源于stack exchange，提问作者the_martian