如何在 Dafny 中导致无效的 LogicalExpression？答案

【问题标题】：How to result invalid LogicalExpression in Dafny?如何在 Dafny 中导致无效的 LogicalExpression？
【发布时间】：2021-10-04 21:05:43
【问题描述】：

考虑下面的 dafny 函数：

function method unpair(n: nat): (nat, nat)
{
  var x,y :| n == (x+y)*(x+y+1)/2 + y;
  return (x,y)
}

给定一个自然数 n，我想确定 2 个满足方程 (x+y)*(x+y+1)/2 + y 的自然数 x 和 y。使用 Cantor 的配对函数可以做到这一点，但不确定我是否有正确的语法，因为 dafny 抛出错误：返回行上的“无效 LogicalExpression”。我该如何解决这个错误？

【问题讨论】：

【解决方案1】：

function method 是（可能令人困惑）function，唯一的区别是它允许从非幽灵上下文中调用。在任何function（包括function methods）中，我们不需要在Dafny 中说return。相反，函数体只是我们想要返回的表达式。所以你应该写

function method unpair(n: nat): (nat, nat)
{
  var x,y :| n == (x+y)*(x+y+1)/2 + y;
  (x,y)
}

此时，您拥有一个语法有效的函数。

然后，Dafny 抱怨了几个语义问题。首先，有一些关于“不满足nat 类型的约束”的错误。您可以通过显式声明x 和y 来修复这些问题，使其具有nat 类型，如下所示：

function method unpair(n: nat): (nat, nat)
{
  var x:nat,y:nat :| n == (x+y)*(x+y+1)/2 + y;
  (x,y)
}

此时，Dafny 又报告了一个错误，即它不能证明一直存在x 和y 这样的一个。这是一个更根本的问题。您需要说服 Dafny（可能使用单独的引理）这样的数字总是存在的。

【讨论】：