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

ダフニーfunctionは純粋です。彼らはreads節を与えることによって、ヒープに依存することができます。しかし、彼らは副作用を持つことはできません - 彼らはヒープを変更することはできません。関数fooは引数がゼロで、reads句はないので、呼び出されるたびに同じ値を返す必要があります。メモリ割り当て演算子newは呼び出されるたびに異なる値を与えるため、関数内で使用することはできません。

Dafnyの機能はデフォルトでghostであることに注意することも重要です。実行時に実行可能ではありません。むしろそれらはコンパイルの検証段階で使用されます。ゴースト以外の機能が必要な場合は、functionの代わりにfunction methodと書く必要があります。

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); 
}