如何在Dafny中移除map<U, V>类型中的元素？

Dafny 里的 map<U, V> 是不可变数据结构——你没法直接修改原 map 的内容，移除元素本质是创建一个不包含目标键的新 map。下面是两种常用的实现方式：

方法一：通过 map 推导式过滤 #

直接遍历原 map 的所有键，只保留不等于目标键的条目来构建新 map：

method RemoveKeyFromMap<K, V>(originalMap: map<K, V>, keyToRemove: K) returns (newMap: map<K, V>)
{
    newMap := map k | k in originalMap && k != keyToRemove :: originalMap[k];
}

方法二：利用键集合的差集操作 #

先获取原 map 的键域（Dom），通过集合差集去掉要移除的键，再基于新的键集合构建 map：

method RemoveKeyFromMap<K, V>(originalMap: map<K, V>, keyToRemove: K) returns (newMap: map<K, V>)
{
    var newKeyDomain := originalMap.Dom - {keyToRemove};
    newMap := map k in newKeyDomain :: originalMap[k];
}

注意事项 #

• 如果要移除的键本来就不在原 map 里，两种方法都会返回和原 map 完全一致的新实例，不会抛出错误。
• 由于 map 不可变，原 map 会始终保持修改前的状态，所有操作都是生成新的 map 对象。

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