Dafny中Map操作问题：closureRemoveInMap函数断言无法证明

已验证的单个元素移除函数 #

我先实现了单个键的移除函数removeInMap，并完成了验证：

function removeInMap(w: string, m: map<string, int>): map<string, int>
{
    map x: string | x in m  && x != w :: m[x]
}

method checkRemoveInMap() 
{
    var m: map<string, int>:= map["aa":= 0, "ab" := 1];
    var newM1:= removeInMap("aa", m);
    assert |m.Keys| == 2;
    assert m["aa"] == 0;
    assert "ab" in newM1;
    assert newM1["ab"] == 1;
    assert !("aa" in newM1);
    var newM2:=  removeInMap("bb", newM1);
    assert "ab" in newM2;
    assert !("aa" in newM2);
    assert newM1 == newM2;
 }

这段代码的所有断言都能被Dafny成功验证。

泛化的递归批量移除函数 #

接着我把函数泛化为递归形式，实现批量移除序列中的键：

function closureRemoveInMap(s: seq<string>, m: map<string, int>): map<string, int>
{
   if |s| == 0 then m else closureRemoveInMap(s[1..], removeInMap(s[0], m))
}

验证失败的测试方法 #

但在验证批量移除的测试方法时，Dafny无法证明最后三个断言：

method checkClosureRemoveInMaps() 
{
    var m: map<string, int>:= map["aa":= 0, "ab" := 1];
    var newM:= closureRemoveInMap(["aa", "bb"], m);
    assert |m.Keys| == 2;
    assert m["aa"] == 0;
    assert "ab" in newM;       // 无法证明
    assert newM["ab"] == 1;    // 无法证明
    assert !("aa" in newM);    // 无法证明
}

原因分析 #

Dafny的自动验证器无法自动推导递归函数的所有隐含性质，核心问题在于：

• 递归函数closureRemoveInMap没有明确的契约（前置/后置条件），验证器不知道递归调用后哪些键会被保留、哪些会被移除，也不清楚值的对应关系
• 对于递归结构，验证器需要明确的归纳线索才能完成证明，而无契约的递归函数无法提供这些线索

解决方法 #

1. 给递归函数添加后置条件 #

通过ensures子句明确函数的行为，告诉验证器最终结果的键值关系：

function closureRemoveInMap(s: seq<string>, m: map<string, int>): map<string, int>
    // 最终Map的键是原Map中不在输入序列里的键
    ensures forall k: string :: k in result <==> (k in m && k !in s)
    // 保留的键对应的值和原Map一致
    ensures forall k: string :: k in result ==> result[k] == m[k]
{
   if |s| == 0 then m else closureRemoveInMap(s[1..], removeInMap(s[0], m))
}

添加这两个后置条件后，Dafny就能通过归纳自动证明所有断言。

2. 编写辅助归纳引理 #

如果复杂场景下后置条件不够，还可以编写lemma来证明递归步骤的性质，比如证明批量移除的结合性：

lemma closureRemoveAppend(s: seq<string>, w: string, m: map<string, int>)
    ensures closureRemoveInMap(s + [w], m) == removeInMap(w, closureRemoveInMap(s, m))
{
    if |s| == 0 {
        assert closureRemoveInMap([w], m) == removeInMap(w, m);
    } else {
        closureRemoveAppend(s[1..], w, m);
        assert closureRemoveInMap(s + [w], m) == closureRemoveInMap(s[1..] + [w], removeInMap(s[0], m));
    }
}

在测试方法中调用这个引理，就能辅助验证器完成证明。

3. 改用迭代实现 #

如果递归的证明成本太高，也可以把函数改成迭代式的方法，通过循环不变量让验证器更容易推导：

method closureRemoveInMapIter(s: seq<string>, m: map<string, int>) returns (result: map<string, int>)
    ensures forall k: string :: k in result <==> (k in m && k !in s)
    ensures forall k: string :: k in result ==> result[k] == m[k]
{
    result := m;
    var i := 0;
    while i < |s|
        invariant forall k: string :: k in result <==> (k in m && k !in s[0..i])
        invariant forall k: string :: k in result ==> result[k] == m[k]
    {
        result := removeInMap(s[i], result);
        i := i + 1;
    }
}

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