Контекст Dafny изменяет ошибку предложения

Мне очень трудно избавиться от последней ошибки в моей программе Dafny. Может ли кто-нибудь указать мне в правильном направлении? Вот код: http://rise4fun.com/Dafny/2FPo

Я получаю эту ошибку: присваивание может обновить элемент массива не в предложении модификаций окружающего контекста

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

Я действительно потерян на этом. Спасибо за помощь


dafny
person Adrien Pecher    schedule 24.04.2017    source источник

Ответы (1)


arrow_upward
7
arrow_downward

Проблема в том, что «изменяет это» позволяет изменять поля этого, а не изменять вещи, на которые указывают эти поля. Другими словами, было бы уместно, если бы метод делал:

this.rectangles := new_rectangle_array;

но не если бы он делал:

this.rectangles[3] := new_rect;

Итак, в местах, где у вас есть «изменить это», вы должны вместо этого «изменить прямоугольники».

По той же причине Test необходимо аннотировать «модифицирует c.rectangles», а не «модифицирует c».

Наконец, чтобы убедить Дафни в том, что вызывать Test можно, нужно задать конструктору Couverture постусловие, ограничивающее поле прямоугольников. В противном случае верификатор не может быть уверен, что можно вызвать Test: насколько может судить верификатор, couv может содержать какой-то случайный массив, который Main не разрешено изменять.

Полный код см. на странице http://rise4fun.com/Dafny/Skrg.

person Jay Lorch    schedule 25.04.2017
comment
В итоге нашел, но все равно спасибо! Очень красивое объяснение проблемы. Это обязательно поможет мне в будущем - person Adrien Pecher; 25.04.2017