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

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

В Dafny function s являются чистыми. Они могут зависеть от кучи, давая оговорку 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); 
}