错误“赋值可能会更新不在封闭上下文的修改子句中的对象”

Question

我必须创建一个包含匿名构造函数的类，一个创建 PrimeBuffer 对象的命名构造函数 CreatePrimeBuffer(primes: seq)，以及一个方法 CheckPrime(n: nat) returns (p: bool) 检查 n 是否为主要的。它检查数据库并使用该结果（如果该结果在数据库中）。如果数据库中没有该数字，则计算该数字是否为素数（使用下面的IsPrime方法），如果是素数则将该数字添加到数据库中并返回结果。到目前为止，我已经做到了：

class PrimeBuffer{
    var s: set<nat>
constructor()
ensures |s|==0
{
    s:={};
}
method CheckPrime(n: nat) returns (p: bool)
modifies s
{
    if n in s {p:=true;}
    else {p:= IsPrime(n);
        if p==true {s:=s+{n};}
    }
    
}
constructor CreatePrimeBuffer(primes: seq<nat>)//no funcional
//ensures |primes| == |s|
//ensures forall i | 0<=i< |primes| :: primes[i] in s
{
   s := set x:nat | x in primes :: x;
    //assert |primes| == |s|;
    // var i:=0;
    // while i< |primes|

    // {
    //     s:=s+{primes[i]};
    //     i:=i+1;
    // }
}
}
ghost predicate prime (n: nat)
{n>1 && ( forall d | 1 < d < n :: n % d != 0) }

method IsPrime ( n: nat ) returns ( p: bool )

{
    p:=true;
    var i:=0;
    while i< (n/2)
    {
        if i%n != 0 {p:=false;}
        i:=i+1;
    }
}

但是 CheckPrime 方法在“s:=s+{n};”上打印错误如何将一个 nat 添加到我的一组 nat 中？

我尝试了不同的方法，但它们都遇到了同样的问题。

Answer 1

你真正想要的并不是

modifies s

但是

modifies this

或

modifies this`s

Modizes 谈论哪些内存位置，并且您可以在 Dafny 中指定的唯一内存位置是整个引用对象（其所有字段），如第一个修改中，或单个字段，如第二个示例中。