Обновление карты другой картой в Дафни

Я хотел бы написать следующую функцию в Dafny, которая обновляет карту m1 всеми сопоставлениями из m2, так что m2 переопределяет 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 оба имеют конечные домены, то их объединение тоже конечно конечно, но как я могу объяснить это Дафни?

ОБНОВЛЕНИЕ:

После применения исправлений Джеймса работает:

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
person Samuel Gruetter    schedule 02.10.2018    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Хорошие вопросы! Вы сталкиваетесь с некоторыми известными острыми краями в Дафни, которые недостаточно задокументированы.

В первой ошибке Дафни в основном говорит, что переменная типа K должна быть ограничена, чтобы она не была ссылочным типом. Вы можете сделать это, изменив сигнатуру функции, чтобы начать с

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

Здесь (!new) - это синтаксис Дафни, означающий, что K может быть создан только с типами значений, а не ссылочными типами. (К сожалению, !new еще не задокументировано, но по этому поводу существует открытая проблема. )

Во второй ошибке вы нарушаете ограниченную синтаксическую эвристику Дафни, чтобы доказать конечность, как описано в этом вопрос и ответ. Исправление состоит в том, чтобы использовать встроенный в Dafny оператор объединения множеств вместо логической дизъюнкции, например:

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

(Здесь я использую .Keys для преобразования каждой карты в набор ключей в ее домене, чтобы я мог применить +, который работает с наборами, но не с картами.)

Теперь, когда эти две ошибки времени проверки типа исправлены, вы получаете две новые ошибки времени проверки. Ура!

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

Они говорят вам, что утверждение самого постусловия неправильно сформировано, потому что вы индексируете карты, используя ключи, не предполагая должным образом, что эти ключи находятся в домене карты. Это можно исправить, добавив еще одно постусловие (перед остальными), например:

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

После этого вся функция проверяется.

person James Wilcox    schedule 02.10.2018
comment
Спасибо, теперь все понятно! На самом деле я пытался использовать K(!new), но вставил его в forall k : K(!new) :: ..., что не сработало. - person Samuel Gruetter; 03.10.2018
comment
Дополнительный вопрос: stackoverflow.com/questions/52618673 / - person Samuel Gruetter; 03.10.2018