Dafny：构造函数中的后置条件错误答案

【问题标题】：Dafny: Postcondition error in constructorDafny：构造函数中的后置条件错误
【发布时间】：2020-05-26 14:42:34
【问题描述】：

以下构造函数不起作用并失败

parent !in 代表

为什么 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};
}

【问题讨论】：

标签： dafny

【解决方案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

【讨论】：

谢谢！ HashObj 是一个 trait，但 Node 没有扩展这个或任何其他 trait。
它解决了这个方法中的问题，但在其他代码位置引起了额外的问题。因此我选择了不同的方法。