在生成的代码中检查任何前提条件

Question

我想知道是否有一种方法可以在Dafny生成的代码中添加前提条件检查。例如，让我们看下面的代码片段:

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
requires 0 < y
ensures less < x < more
{
more := x + y;
less := x - y;
}

我希望c++中的结果代码具有以下检查:

assert(0 < y);

如果这在Dafny中不可用，我有什么选择?谢谢你！

Answer 1

没有自动将requires子句转换为运行时检查的方法。requires子句的条件是在一个幽灵上下文中，所以它通常是不可编译的。同样，如果你验证了你的程序，那么你就知道条件总是会求值为true，所以在运行时也检查它是没有意义的。

为了支持要检查的条件难以静态验证的情况，特别是支持调用者不是用Dafny编写的跨语言情况，因此不需要验证，Dafny有expect语句。您可以在示例中使用expect将静态验证的前提条件转换为运行时检查:

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
ensures less < x < more
{
RuntimeRequires(0 < y);
more := x + y;
less := x - y;
}
method RuntimeRequires(cond: bool)
ensures cond
{
expect cond, "precondition failure";
}

请注意，如果没有requires子句，您将无法在调用站点获得任何静态验证。

作为另一种变体，您可以同时使用requires子句和我所展示的RuntimeRequires方法。如果您这样做，我建议您将RuntimeRequires的规格从ensures更改为requires，以确保您正确地复制了条件。

method MultipleReturns(x: int, y: int) returns (more: int, less: int)
requires 0 < y
ensures less < x < more
{
RuntimeRequires(0 < y); // try changing this to 10 < y and see what happens
more := x + y;
less := x - y;
}
method RuntimeRequires(cond: bool)
requires cond
{
expect cond, "precondition failure";
}