Dafny:构造函数中的后置条件错误

Question

以下构造函数不起作用，并且在

父级 ！in Repr

为什么Dafny不能证明后置条件，即父项不是Repr集的一部分？

constructor Init(x: HashObj, parent:Node?)
ensures Valid() && fresh(Repr - {this, data})
ensures Contents == {x.get_hash()}
ensures Repr == {this, data};
ensures left == null;
ensures right == null;
ensures data == x;
ensures parent != null ==> parent !in Repr;
ensures this in Repr;
{
data := x;
left := null;
right := null;
Contents := {x.get_hash()};
Repr := {this} + {data};
}

Answer 1

我猜HashObj是trait？(如果是class，那么您的示例为我验证。验证失败，因为验证者认为x可能等于parent。

验证者应该知道Node不是HashObj(当然，除非你的类Node确实扩展了HashObj(，但它没有。您可以将其作为 https://github.com/dafny-lang/dafny 的问题提交以更正。

同时，你可以写一个前提条件，说明x和parent是不同的。在这里，也有皱纹。你想写

requires x != parent

但是(除非Node真的扩展了HashObj(这不会进行类型检查。因此，您可能希望将parent投射到object?。这种向上转换没有直接语法，但您可以使用 let 表达式来完成：

requires x != var o: object? := parent; o