Dafny迭代方法中无法验证Map修改序列的问题求助

我在Dafny中编写了一个迭代方法，用于验证Map中的一系列更新操作，但Dafny无法证明关键的不变式和后置条件。目前所有断言都能被正确证明，但最后一个不变式始终无法通过验证。

代码如下：

function updateMap(t: (bool, string, int), m: map<string, int>): map<string, int>
  requires t.1 in m
  ensures forall k :: k in m <==> k in updateMap(t, m)
  ensures t.0 ==> updateMap(t, m)[t.1] == t.2
{
  if t.0 then m[t.1:=t.2] else m
}

method updateMapIterative(s: seq<(bool, string, int)>, m: map<string, int>) returns (r: map<string, int>)
  requires forall t: (bool, string, int) :: t in s ==> t.1 in m
  ensures forall k :: k in m <==> k in r
  ensures forall t: (bool, string, int) :: t in s && t.0 ==> r[t.1] == t.2 //Can't prove this
{

  r := m;
  var i := 0;

  while i < |s|
    decreases |s|-i
    invariant 0 <= i <= |s|
    invariant forall t: (bool, string, int) :: t in s[0..i] ==> t.1 in r
    invariant forall k :: k in m <==> k in r
    invariant forall t: (bool, string, int) :: t in s[0..i] && t.0 ==> r[t.1] == t.2 //Can't prove this invariant
  {
    assert s[i].1 in m;
    r:= updateMap(s[i], m);
    assert s[i].0 ==> r[s[i].1] == s[i].2;
    i := i + 1;
    assert s[i-1].1 in m;
    assert s[i-1].0 ==> r[s[i-1].1] == s[i-1].2;
  }
}

问题原因 #

循环体中更新r时，错误地传入了初始的m而非当前的r。updateMap(s[i], m)会基于原始Map执行修改，而非在当前迭代后的r基础上更新。这导致之前迭代的修改被覆盖，无法维护“前i个元素的更新都已应用到r”的不变式——每次循环只保留了当前元素对原始Map的修改，而非累积所有之前的更新。

修正代码 #

将循环内的r:= updateMap(s[i], m);改为r:= updateMap(s[i], r);，确保每次迭代都在当前r的基础上应用新的更新：

function updateMap(t: (bool, string, int), m: map<string, int>): map<string, int>
  requires t.1 in m
  ensures forall k :: k in m <==> k in updateMap(t, m)
  ensures t.0 ==> updateMap(t, m)[t.1] == t.2
{
  if t.0 then m[t.1:=t.2] else m
}

method updateMapIterative(s: seq<(bool, string, int)>, m: map<string, int>) returns (r: map<string, int>)
  requires forall t: (bool, string, int) :: t in s ==> t.1 in m
  ensures forall k :: k in m <==> k in r
  ensures forall t: (bool, string, int) :: t in s && t.0 ==> r[t.1] == t.2
{

  r := m;
  var i := 0;

  while i < |s|
    decreases |s|-i
    invariant 0 <= i <= |s|
    invariant forall t: (bool, string, int) :: t in s[0..i] ==> t.1 in r
    invariant forall k :: k in m <==> k in r
    invariant forall t: (bool, string, int) :: t in s[0..i] && t.0 ==> r[t.1] == t.2
  {
    assert s[i].1 in m;
    r:= updateMap(s[i], r); // 此处改为传入当前的r
    assert s[i].0 ==> r[s[i].1] == s[i].2;
    i := i + 1;
  }
}

修正说明 #

修改后，每次迭代都会基于当前的r应用新的更新操作，保证了不变式的归纳性：

1. 初始时i=0，r=m，不变式成立；
2. 假设循环前不变式成立（前i个元素的更新已应用到r），循环中用当前r更新后，新的r包含前i+1个元素的所有更新，不变式得以维护；
3. 循环结束时i=|s|，不变式直接推导出后置条件。

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