Dafny işlevinde neden yeni bir hata veriyor? Aşağıdaki program için bir hata alıyorum neden merak ediyorum

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

I got: invalid UnaryExpression Bunu çalıştırdığınızda. Dafny function da saftır.

Answer 1

reads maddesini vererek yığına güvenebilirler. Ancak yan etkilere sahip olamazlar - öbekleri değiştiremezler. foo işleviniz sıfır bağımsız değişkenlere ve reads numaralı maddeye sahip olduğundan, her çağrıldığında aynı değeri döndürmelidir. Bellek ayırma operatörü new, her çağrıldığında farklı bir değer verir, bu nedenle bir işlevde kullanılamaz.

Dafny işlevlerinin varsayılan olarak ghost olduğunu unutmamak da önemlidir. Çalışma zamanında yürütülebilir değiller. Aksine, derlemenin doğrulama aşamasında kullanılır. Hayalet olmayan bir işlev istiyorsanız, function yerine function method yazmalısınız.

method'un içinde new'u kullanabilirsiniz. Yöntemler zorunlu prosedürlerdir ve saf olması gerekmez.

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