Dafny 前置条件检查生成的代码

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";
}

Dafny 前置条件检查生成的代码

Dafny precondition checks in generated code

preconditions

dafny