Whiley验证向量加法函数时提示v1[i]可能索引越界是何原因

你写的向量加法代码运行时不会出现真实越界，但静态验证器无法推导索引合法性，因此抛出错误。
你当前编写的代码如下：

function add(int[] v1, int[] v2) -> (int[] v3)
requires |v1| == |v2|
ensures |v3| == |v1|:
    //
    v3 = v1
    //
    for i in 0..|v3|:
        v3[i] = v1[i] + v2[i]
    //
    return v3

报错根因 #

• 核心问题是数组引用别名：Whiley中数组是引用语义，v3 = v1会让两个变量指向同一个数组实例，而非创建独立副本。当你在循环中修改v3的元素时，静态验证器会保守判定数组的长度约束可能在修改过程中失效，不会自动把函数开头的|v1| == |v2|前置条件关联到循环内的v1[i]访问上。
• 验证器对可变数组的循环检查默认持保守策略：你没有明确给出循环不变式来约束迭代过程中三个数组的长度始终一致，它无法确认每次循环时i一定落在v1的合法索引范围内，因此判定存在越界风险。

修复方式 #

方式1：补充循环不变式（保留原有赋值逻辑） #

给循环添加where子句明确不变式，告诉验证器长度约束在整个循环过程中始终成立：

function add(int[] v1, int[] v2) -> (int[] v3)
requires |v1| == |v2|
ensures |v3| == |v1|:
    //
    v3 = v1
    //
    for i in 0..|v3|
    where |v1| == |v2| && |v3| == |v1| && i <= |v3|:
        v3[i] = v1[i] + v2[i]
    //
    return v3

方式2：初始化独立新数组（更推荐） #

从根源避免数组别名问题，初始化一个和v1等长的新数组作为v3，不需要额外写不变式就能通过验证，也更符合向量加法返回新数组的语义：

function add(int[] v1, int[] v2) -> (int[] v3)
requires |v1| == |v2|
ensures |v3| == |v1|:
    // 创建固定长度的独立数组，不和输入参数产生引用别名
    v3 = [0; |v1|]
    //
    for i in 0..|v3|:
        v3[i] = v1[i] + v2[i]
    //
    return v3

补充说明：Whiley中0..n表示从0到n-1的左闭右开区间，迭代范围本身是合法的，问题核心还是引用别名和缺少循环不变式导致验证器无法推导索引合法性。

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