Dafny过滤元音时出现Postcondition可能不成立及下标越界错误求助

两个报错的根因 #

• 索引越界报错：辅助方法countTheVowels的后置条件过弱，Dafny无法证明你统计出来的count就是数组内元音的总个数，自然无法证明循环内j的取值永远小于vowels的长度（即count），因此判定vowels[j]的访问存在越界风险。
• 后置条件不成立报错：你写的后置条件逻辑本身存在语义缺陷，同时循环不变式没有覆盖足够的状态约束，Dafny无法推导循环结束后状态符合后置条件要求。

具体修复步骤 #

1. 补全countTheVowels的约束 #

给辅助方法补充准确的后置条件与循环不变式，让Dafny确认返回的count确实等于输入数组中元音字符的总数量：

method countTheVowels(a: array<char>) returns (count: int)
requires a.Length > 0
ensures count >= 0
// 新增后置条件：count等于数组中所有元音的数量
ensures count == |set i | 0 <= i < a.Length && a[i] in ['a','e','i','o','u']|
{
    count := 0;
    var i := 0;
    while i < a.Length
    invariant 0 <= i <= a.Length
    // 新增循环不变式：前i个元素中元音的数量等于当前count
    invariant count == |set k | 0 <= k < i && a[k] in ['a','e','i','o','u']|
    {
        if a[i] in ['a','e','i','o','u'] {
            count := count + 1;
        }
        i := i + 1;
    }
}

2. 补全filterTheVowels的循环不变式与后置条件 #

首先修正后置条件的语义，你的需求是过滤得到所有元音，因此后置条件需要明确：返回数组的所有元素都是元音，且与原数组中的元音总数匹配。其次新增循环不变式，证明j的取值永远合法：

method filterTheVowels(a: array<char>) returns (vowels: array<char>)
requires a.Length > 0
// 修正后置条件1：返回数组所有元素都是元音
ensures forall j | 0 <= j < vowels.Length :: vowels[j] in ['a','e','i','o','u']
// 修正后置条件2：返回数组的长度等于原数组元音总数
ensures vowels.Length == |set i | 0 <= i < a.Length && a[i] in ['a','e','i','o','u']|
{
    var count := countTheVowels(a);
    vowels := new char[count];
    var i := 0;
    var j := 0;
    while i < a.Length
    invariant 0 <= i <= a.Length
    invariant 0 <= j <= count
    // 新增不变式：j等于前i个元素中的元音数量，证明j不会超过count
    invariant j == |set k | 0 <= k < i && a[k] in ['a','e','i','o','u']|
    invariant forall l | 0 <= l < j :: vowels[l] in ['a','e','i','o','u']
    {
        if a[i] in ['a','e','i','o','u'] {
            vowels[j] := a[i]; 
            j := j + 1;
        }
        i := i + 1;
    }
}

3. 验证结果 #

修改完成后重新运行Dafny验证，两个报错都会消失，原Main方法的执行结果会正确输出3（对应示例数组中的3个'e'）。

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