如何提升Dafny断言验证能力？解决字符串包含谓词验证失败问题

定义的Contains谓词 #

predicate Contains(haystack: string, needle: string)
    ensures Contains(haystack, needle) <==> exists k :: 0 <= k <= |haystack| && needle <= haystack[k..] 
    ensures Contains(haystack, needle) <==> exists i :: 0 <= i <= |haystack| && (needle <= haystack[i..])
    ensures !Contains(haystack, needle) <==> forall i :: 0 <= i <= |haystack| ==> !(needle <= haystack[i..])
{
    if needle <= haystack then 
        assert haystack[0..] == haystack;
        true 
    else if |haystack| > 0 then 
        assert forall i :: 1 <= i <= |haystack| ==> haystack[i..] == haystack[1..][(i-1)..];
        Contains(haystack[1..], needle)
    else 
        false
}

测试代码及验证异常 #

method TestContains() {
    assert Contains("aba||xx||c", "|") == true; //验证通过
    assert Contains("aba||xx||c", "||") == true; //验证通过
    assert Contains("aba||xx||c", "||xx||") == true; //验证通过
    assert Contains("aba||xx||c", "|||") == false; //无法验证
}

问题表现 #

• 所有判定为true的案例能快速验证通过；
• 单字符匹配失败的案例（如Contains("aa", "b")）可正常验证；
• 多字符匹配失败的案例（如Contains("axa", "ba")、Contains("aba||xx||c", "|||")）无法被Dafny判定真假；
• 尝试使用{:fuel X}属性调整验证资源，未解决问题。

解决办法 #

1. 补充字符串后缀匹配的关键引理 #

Dafny自动验证器对多字符后缀的全称量化推理能力有限，需要手动补充引理明确规则。比如添加以下引理，帮验证器理解“若长字符串不是短字符串的前缀，则短字符串不可能匹配长字符串的任何后缀”：

lemma NotPrefixImpliesNotSuffixMatch(haystack: string, needle: string)
    requires |needle| > |haystack| || !(needle[0..|haystack|] == haystack)
    ensures !(needle <= haystack)
{}

在Contains谓词的递归分支中引用这类引理，引导验证器完成推理。

2. 重构谓词实现，显式遍历起始位置 #

原递归实现依赖后缀隐式遍历，验证器难完成否定推理。改成显式检查每个可能的起始索引，明确“包含”的语义为“存在某个起始位置，对应切片与needle相等”：

predicate Contains(haystack: string, needle: string)
    ensures Contains(haystack, needle) <==> exists k: nat :: k + |needle| <= |haystack| && haystack[k..k+|needle|] == needle
{
    if |needle| == 0 then
        true
    else if |haystack| < |needle| then
        false
    else
        haystack[0..|needle|] == needle || Contains(haystack[1..], needle)
}

这种实现让验证器处理否定案例时，能直接检查所有可能的切片是否不匹配，减少递归带来的推理负担。

3. 为测试案例添加辅助断言 #

对无法自动验证的false案例，手动添加中间断言拆解验证步骤，给验证器提供线索。比如针对Contains("aba||xx||c", "|||") == false：

method TestContains() {
    // ... 其他断言
    assert forall k: nat :: k + 3 <= |"aba||xx||c"| ==> "aba||xx||c"[k..k+3] != "|||";
    assert Contains("aba||xx||c", "|||") == false;
}

通过显式列出所有可能切片都不匹配，帮助验证器完成最终判定。

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