dafny - Dafny 上下文修改子句错误

Question

我很难摆脱 Dafny 程序中的最后一个错误。有人可以指出我正确的方向吗？这是代码：http ://rise4fun.com/Dafny/2FPo

我收到此错误：赋值可能会更新不在封闭上下文的修改子句中的数组元素

我尝试在合并方法中添加修改矩形（即使我很确定它已经包含在修改此中）但这只会在合并方法调用中产生类似的错误。

我真的迷失了这个。谢谢您的帮助

Answer 1

问题是“修改 this”允许修改 this 的字段，而不是修改这些字段指向的内容。换句话说，如果该方法正在执行以下操作是合适的：

this.rectangles := new_rectangle_array;

但如果它在做：

this.rectangles[3] := new_rect;

所以，在你有“修改这个”的地方，你应该有“修改矩形”。

出于类似的原因，Test 需要用“modifies c.rectangles”而不是“modifies c”来注释。

最后，为了说服 Dafny 可以调用 Test，您需要为 Couverture 的构造函数提供一个约束矩形字段的后置条件。否则，验证者无法确定调用 Test 是否正常：据验证者所知，couv 可能包含一些 Main 不允许修改的随机数组。

有关完整代码，请参阅http://rise4fun.com/Dafny/Skrg。