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

如何解决Dafny 前提条件检查生成的代码

我想知道是否有办法在 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 中不可用，我有哪些选择？谢谢！

解决方法

没有自动将 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,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";
}