Dafny Call может нарушать условие изменения контекста

Я пытаюсь проверить хэш-набор, но у меня возникла проблема с моим методом вставки.

Я не понимаю, почему я получаю сообщение об ошибке «вызов может нарушить условие изменения контекста», когда я раскомментирую вставки в main. Я считаю, что это как-то связано с использованием свежих, но я не понимаю, как/где это сделать.

Код можно найти по адресу: https://rise4fun.com/Dafny/9UDG.


dafny
person DeirdreCleary    schedule 22.11.2017    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Проблема в том, что вставка требует изменить this и a, что оставляет открытой возможность того, что первый вызов insert изменяет поле a так, чтобы оно указывало на что-то произвольное, а затем второй вызов insert изменяет эту произвольную вещь.

Простое решение — добавить ensures a == old(a) к insert.

person James Wilcox    schedule 23.11.2017