Frama-C/WP验证移动平均函数时数组切片指针有效性证明失败求助

嗨，我仔细排查了你的代码和遇到的问题，你卡在这里的核心原因其实是两个容易忽略的细节：权限谓词不匹配，以及循环里缺少关键不变式帮WP理清数组区间的关联。下面给你一步步拆解问题和修复方案：

一、问题根源分析 #

1. 权限要求错配：sum函数要了没必要的可写权限 #

你的sum函数声明里第一个前置条件是\valid(values+(0..length-1))，这个谓词要求数组元素具备可写权限，但sum函数的assigns \nothing明确说明它不会修改任何内容，只需要读取权限就够了。而在moving_average_filter里，你给raw_data的权限是\valid_read（通过valid_array_r谓词），这和sum要求的\valid不兼容，WP自然无法证明这个前置条件。

2. 循环缺少关键关联：WP无法自动推导数组区间的合法性 #

在moving_average_filter的循环中，虽然从逻辑上看：

• i的范围是0<=i < filtered_data_length
• 而filtered_data_length = raw_data_length - window_size +1
• 所以i + window_size -1 <= raw_data_length -1，正好落在raw_data的有效区间内

但WP不会自动帮你推导这个链式关系，必须把i和raw_data有效区间的关联作为循环不变式明确写出来，它才能认可raw_data+i开始的window_size个元素是合法的。

二、具体修复步骤 #

1. 修正sum函数的权限前置条件 #

把sum函数的valid_array前置条件从\valid改成\valid_read，因为它只需要读取数组：

/*@ requires valid_array: \valid_read(values+(0..length-1));
  requires valid_length: 0<=length<=50;
  requires valid_range: \forall integer i; 0<= i < length ==> 0<=values[i]<=MAX_VOLTAGE;
  assigns \nothing;
  ensures \result == sum(values, length);
*/
int sum(int *values, unsigned int length) {
  // 函数体保持不变
}

2. 给moving_average_filter的循环添加关键不变式 #

在循环的不变式列表里，加上两个关键项，帮WP明确数组区间的合法性：

/*@ loop invariant 0 <= i <= filtered_data_length;
  loop invariant \forall integer k; 0 <= k < i ==> filtered_data[k]==average(raw_data+k, window_size);
  loop invariant \forall integer k; 0 <= k < i ==> 0 <= filtered_data[k] <= MAX_VOLTAGE;
  // 新增：确保当前i对应的window完全落在raw_data的有效范围内
  loop invariant i + window_size <= raw_data_length;
  // 新增：明确raw_data从i开始的window_size个元素可读
  loop invariant \valid_read(raw_data + (i .. i + window_size - 1));
  loop assigns i, filtered_data[0..i];
  loop variant filtered_data_length - i;
*/
for (unsigned int i = 0; i < filtered_data_length; i++) {
  filtered_data[i] = sum(raw_data+i, window_size)/window_size;
}

其中第一个新增的不变式是核心，它直接把i的范围和raw_data_length、window_size绑定起来，第二个不变式是辅助WP快速定位权限，有了第一个其实也能推导，但写出来会更稳妥。

3. 可选：添加调用前的断言辅助（如果还是有问题） #

如果修改后还有个别验证点卡住，可以在调用sum前加一个断言，帮WP明确当前的数组区间合法性：

for (unsigned int i = 0; i < filtered_data_length; i++) {
  /*@ assert \valid_read(raw_data + i .. i + window_size -1); */
  filtered_data[i] = sum(raw_data+i, window_size)/window_size;
}

不过一般来说，有了前面的循环不变式，这个断言不是必须的。

三、额外优化建议 #

1. 统一整数类型：sum的length是unsigned int，但你的逻辑谓词里用的是integer，虽然WP能处理，但尽量保持类型一致可以避免潜在的隐式转换问题。
2. 整数除法的一致性：你的average逻辑函数用的是C风格的整数除法（向零取整），代码里也是这么实现的，这点没问题，但要确保后续需求变化时，spec和代码行为始终对齐。
3. sum函数的循环不变式：你的sum函数的循环不变式写得很规范，这部分没问题，不用修改。

做完这些修改后，用Alt-Ergo或Z3重新验证，所有的前置条件、循环不变式和后置条件应该都能顺利通过证明。

内容来源于stack exchange