在达夫尼用另一张地图更新地图 [英] Updating a map with another map in Dafny

问题描述

我想在Dafny中编写以下函数，该函数将使用 m2 m1 >，这样 m2 会覆盖 m1 ：

I'd like to write the following function in Dafny, which updates a map m1 with all mappings from m2, such that m2 overrides m1:

function update_map<K, V>(m1: map<K, V>, m2: map<K, V>): map<K, V>
ensures
  (forall k :: k in m2 ==> update_map(m1, m2)[k] == m2[k]) &&
  (forall k :: !(k in m2) && k in m1 ==> update_map(m1, m2)[k] == m1[k]) &&
  (forall k :: !(k in m2) && !(k in m1) ==> !(k in update_map(m1, m2)))
{
  map k | (k in m1 || k in m2) :: if k in m2 then m2[k] else m1[k]
}

我遇到以下错误：

Dafny 2.2.0.10923
stdin.dfy(7,2): Error: a map comprehension involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'k' (perhaps declare its type, 'K', as 'K(!new)')
stdin.dfy(7,2): Error: a map comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'k'
2 resolution/type errors detected in stdin.dfy

我不明白第一个错误，第二个错误是 m1 和 m2 都具有有限域，那么它们的并集当然也是有限的，但是我该如何向Dafny解释呢？

I don't understand the first error, and for the second, if m1 and m2 both have finite domains, then their union is certainly finite as well, but how can I explain that to Dafny?

更新：

应用James的修补程序后，它的工作原理是：

After applying James' fixes, it works:

function update_map<K(!new), V>(m1: map<K, V>, m2: map<K, V>): map<K, V>
ensures
  (forall k :: k in m1 || k in m2 ==> k in update_map(m1, m2)) &&
  (forall k :: k in m2 ==> update_map(m1, m2)[k] == m2[k]) &&
  (forall k :: !(k in m2) && k in m1 ==> update_map(m1, m2)[k] == m1[k]) &&
  (forall k :: !(k in m2) && !(k in m1) ==> !(k in update_map(m1, m2)))
{
  map k | k in (m1.Keys + m2.Keys) :: if k in m2 then m2[k] else m1[k]
}

推荐答案

好问题！您遇到的是Dafny中一些已知的未充分记录的尖锐边缘。

Good questions! You are running across some known sharp edges in Dafny that are under-documented.

在第一个错误中，Dafny基本上是在说类型变量需要将K 限制为不是引用类型。您可以通过更改函数签名以

In the first error, Dafny is basically saying that the type variable K needs to be constrained to not be a reference type. You can do that by changing the function signature to start with

function update_map<K(!new), V>...

这里，（！new）是达芙妮语法的含义恰恰是 K 只能用值类型实例化，而不能用引用类型实例化。 （不幸的是，尚未记录！new ，但是有一个

Here, (!new) is Dafny syntax meaning exactly that K may only be instantiated with value types, not reference types. (Unfortunately, !new is not yet documented, but there is an open issue about this.)

在第二个错误中，您违反了Dafny有限的语法试探法来证明有限性，如上所述在此问题和答案中。解决方法是使用Dafny的内置集合并运算符，而不是布尔取和运算符，例如：

In the second error, you are running afoul of Dafny's limited syntactic heuristics to prove finiteness, as described in this question and answer. The fix is to use Dafny's built-in set union operator instead of boolean disjunction, like this:

map k | k in m1.Keys + m2.Keys :: ...

（在这里，我用 .Keys 将每个地图转换为其域中的键集，以便我可以应用 + ，该键可用于集，但

(Here, I use .Keys to convert each map to the set of keys in its domain so that I can apply +, which works on sets but not maps.)

在修复了这两个类型检查时间错误之后，您现在获得了两个新的验证时间错误。

With those two type-checking-time errors fixed, you now get two new verification-time errors. Yay!

stdin.dfy(3,45): Error: element may not be in domain
stdin.dfy(4,59): Error: element may not be in domain

这些告诉您该语句后置条件本身的格式不正确，因为您在使用键索引到地图时没有正确假设这些键在地图的域中。您可以通过添加其他后置条件（在其他条件前 ）来解决此问题，例如：

These are telling you that the statement of the postcondition itself is ill-formed, because you are indexing into maps using keys without properly hypothesizing that those keys are in the domain of the map. You can fix this by adding another postcondition (before the others), like this:

  (forall k :: k in m1 || k in m2 ==> k in update_map(m1, m2)) && ...

此后，整个函数都会验证。

After that, the whole function verifies.

这篇关于在达夫尼用另一张地图更新地图的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！