Frama-C WP无法证明Kadane算法循环不变式的原因排查

问题背景 #

我尝试为求解最大子数组和的Kadane算法添加ACSL注解，并用Frama-C的WP插件验证其正确性，但执行以下命令后，多个循环不变式的保持性目标超时失败：

frama-c -wp -wp-prover Alt-Ergo,Z3 -wp-print -wp-timeout 20 _maximun_subarray.c

使用的Frama-C版本为25.0 (Manganese)。

可能的超时原因分析 #

子数组求和函数的精度问题 #

如果求和函数的ACSL注解未精确刻画其行为（比如未明确区间求和的边界、循环不变式覆盖不足），或者函数实现存在冗余计算，会让SMT prover需要处理更复杂的逻辑推导，直接增加验证时间甚至导致超时。例如，若求和函数的循环不变式未明确说明累加的是数组a[i..j]的区间和，prover可能需要额外推导数组元素的范围关系，大幅提升计算量。

循环不变式设计缺陷 #

Kadane算法的核心循环不变式如果过于宽泛或完备性不足，会导致prover需要验证大量无关逻辑分支。比如未明确当前局部最大子数组和的两种状态（仅包含当前元素，或扩展自之前的子数组），或者未关联全局最大值与局部值的依赖关系，都会让保持性验证的逻辑复杂度飙升，超出超时阈值。

SMT prover的计算限制 #

即使注解和代码逻辑完全正确，某些复杂的数组关系推导对Alt-Ergo或Z3来说计算量极大，20秒的超时设置可能不足以完成推导。比如涉及数组区间的全域量化、多变量的嵌套依赖关系时，prover的搜索空间会呈指数级增长，最终因时间耗尽导致验证失败。

代码与注解的冗余负担 #

代码中不必要的变量、分支，或是注解中多余的断言，都会分散prover的注意力，增加验证负担。例如未简化的中间变量、重复的条件判断，都可能延长验证时间，最终触发超时。

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