1

次のプログラムでエラーが発生する理由を知りたいです。

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これを実行したとき。

4

1 に答える 1

2

Dafny では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);
}
于 2016-04-14T14:17:50.953 に答える