dafny - 为什么在 Dafny 函数中使用 new 会出错？

Question

我想知道为什么我收到以下程序的错误：

class KV 
{
  var key : int;
  var value : int;
  constructor (k: int, v: int) modifies this
  {
    this.key := k;
    this.value := v;
  }
}

function foo () : KV
{
   new KV(0,0)
}

我得到了：invalid UnaryExpression当我运行这个时。

Answer 1

在 Dafnyfunction中是纯粹的。reads通过给出一个子句，它们可以依赖于堆。但它们不能有副作用——它们不能修改堆。由于您的函数foo具有零参数且没有reads子句，因此每次调用它时都必须返回相同的值。内存分配运算符new每次调用时都会给出不同的值，因此不能在函数中使用。

同样重要的是要注意ghost默认情况下 Dafny 函数。它们在运行时不可执行。而是在编译的验证阶段使用它们。如果你想要一个非幽灵函数，你必须写function method而不是function.

您可以new在method. 方法是命令式过程，不需要是纯粹的。

class KV 
{
  var key : int;
  var value : int;
  constructor (k: int, v: int) modifies this
  {
    this.key := k;
    this.value := v;
  }
}

method foo () returns (kv:KV)
{
   kv := new KV(0,0);
}