无法证明分配子句 - Frama-C答案

【问题标题】：Unable to prove assign clause - Frama-C无法证明分配子句 - Frama-C
【发布时间】：2013-05-24 17:24:08
【问题描述】：

我是 Frama-c 的新手，我想了解这个简单示例有什么问题：

/*@ requires \valid(array+(0..length-1))
@ ensures \forall integer k; 0 <= k < length ==> array[k] == 0;
@ assigns array[0..length-1];
*/
void fill(int array[], int length){
    /*@ loop invariant 0 <= i <= length;
    @ loop invariant \forall integer k; 0 <= k < i ==> array[k] == 0;
    @ loop assigns i, array[0..i-1];
    @ loop variant length - i;
    */
    for(int i = 0; i < length; i++){
        array[i] = 0;
    }
}

在这个例子中，Frama-c (WP + Value) 不会证明函数合约中的 assign 子句，我不明白为什么。任何帮助将不胜感激 =)

【问题讨论】：

为什么？不好吗？我只想用零填充一个 int 数组（静态声明）...... int * array[] 不是一个 int 指针数组吗？无论如何，它不起作用：/
我不明白你的意思。即使有了这个签名fill(int * array, int length)，问题仍然存在……
@EliasVanOotegem 在 C 中，数组是通过引用传递的。功能不错，规格也不错。 Value 插件不证明“assigns”，因为它不打算这样做（它仅使用“assigns”子句作为信息源，并且仅用于没有源代码的库函数）。我认为 WP 会证明这一点。 Roo，你安装了哪些自动验证器？
由于length 以int 的形式传递，我将添加length 是≥0 或>0 的前提条件（无论您喜欢哪个）。
@PascalCuoq：我的错，我用谷歌搜索了 Frama-C，现在我知道这个问题是关于什么的。这就是为什么我发表评论，而不是写一个冗长的答案。我的印象比我最初想象的要多……

标签： frama-c

【解决方案1】：

如果您削弱循环分配，这可以得到证明（使用 alt-ergo 0.95.1）。

@循环赋值i,array[0..length-1];

还需要前置条件i >= 0，因为它不是由\valid(array+(0..length-1)隐含的。 array+(0..length-1) 是具有length <= 0 的一组有效位置，尽管是一个空位置。

您的原始循环分配的事实并不意味着您的先决条件是 WP 插件当前版本的限制。

【讨论】：

您好鲍里斯，感谢您的回答。我知道我可以通过削弱循环分配来证明这一点，但我想知道为什么它不适用于更强大但正确的子句。感谢您的解释！
如果你喜欢鲍里斯的回答，你应该把它标记为接受（投票按钮下的复选标记）。