Updating a map with another map in Dafny

问题:

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]
}

I got the following errors:

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

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?

UPDATE:

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]
}

回答1:

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

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>...

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.)

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 :: ...

(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.