Почему использование new в функции Dafny дает ошибку?

Мне интересно, почему я получаю сообщение об ошибке для следующей программы:

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, когда запустил это.


dafny
person JRR    schedule 14.04.2016    source источник

Ответы (1)


arrow_upward
2
arrow_downward

В Дафны functionс чисты. Они могут зависеть от кучи, указав предложение reads. Но у них не может быть побочных эффектов — они не могут модифицировать кучу. Поскольку ваша функция foo не имеет аргументов и предложения reads, она должна возвращать одно и то же значение при каждом вызове. Оператор выделения памяти new при каждом вызове дает другое значение, поэтому его нельзя использовать в функции.

Также важно отметить, что функции Dafny по умолчанию имеют значение ghost. Они не исполняются во время выполнения. Скорее они используются на этапе проверки компиляции. Если вам нужна не фантомная функция, вы должны написать 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);
}
person lexicalscope    schedule 14.04.2016