2

我正在尝试验证一个哈希集，但我的插入方法遇到了问题。

我不明白为什么我在取消注释 main 中的插入时收到“调用可能违反上下文的修改子句”错误。我相信这与使用新鲜有关，但我不清楚如何/在哪里这样做。

代码可在以下网址找到：https ://rise4fun.com/Dafny/9UDG

4

1 回答 1

3

问题是 insert 声称要修改thisand a，这留下了第一次调用insert更改a字段以指向任意事物，然后第二次调用insert修改该任意事物的可能性。

一个简单的解决方案是添加ensures a == old(a)到insert.

于 2017-11-23T16:54:54.473 回答