Обновление карты с другой картой в Дафни - PullRequest
Новая
       9

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

0 голосов
/ 02 октября 2018

Я хотел бы написать следующую функцию в 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]
}

Iполучил следующие ошибки: 

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

1 Ответ

0 голосов
/ 02 октября 2018

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

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

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

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

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

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

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

С этими двумя исправленными ошибками времени проверки типов теперь вы получаете две новые ошибки времени проверки.Yay! 

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

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

...