时间戳

首页 > 解决方案 > Dafny：构造函数中的后置条件错误

dafny - Dafny：构造函数中的后置条件错误

问题描述

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

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

解决方案

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

验证者应该知道这Node不是 a HashObj（当然，除非你的类Node确实是 extend HashObj），但事实并非如此。您可以在https://github.com/dafny-lang/dafny上将此作为问题提交以更正。

同时，你可以写一个先决条件，说x和parent不同。在这里，也有皱纹。你想写

requires x != parent

但是（除非Node确实扩展HashObj）这不会进行类型检查。parent所以，你会想投到object?. 这种向上转换没有直接的语法，但您可以使用 let 表达式来实现：

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

推荐阅读