Dafny中PrimeBuffer类CheckPrime方法报错，如何正确更新集合s？

我需要创建一个PrimeBuffer类，包含以下成员：

• 匿名构造函数：初始化空的素数集合
• 命名构造函数CreatePrimeBuffer：接收seq<nat>类型参数，用传入的序列初始化素数集合
• CheckPrime(n: nat)方法：返回bool类型，逻辑为：先检查集合s中是否存在n，存在则返回true；若不存在则调用IsPrime方法判断，若为素数则将n加入集合s并返回结果

编写的代码如下：

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};行出现错误："assignment might update an object not in the enclosing context's modifies clause"，请问如何正确将nat类型元素添加到nat类型集合中？

错误原因 #

Dafny中，类的成员变量属于类实例（对象）的一部分，modifies s的写法不符合语法要求——你需要指定修改的是当前对象，而不是直接写字段名。正确的写法是用modifies this来声明该方法会修改当前实例的成员字段。

另外，你的IsPrime方法存在逻辑错误：

• 循环变量i从0开始没有意义，应该从2开始（1不是素数的因数，0会导致除零错误）
• 判断条件写反了，应该是n % i == 0（如果n能被i整除，说明不是素数）

修正后的完整代码 #

class PrimeBuffer{
    var s: set<nat>

    constructor()
    ensures |s| == 0
    {
        s := {};
    }

    method CheckPrime(n: nat) returns (p: bool)
    modifies this  // 修改为this，表示修改当前对象的字段
    {
        if n in s {
            p := true;
        } else {
            p := IsPrime(n);
            if p {
                s := s + {n};
            }
        }
    }

    constructor CreatePrimeBuffer(primes: seq<nat>)
    ensures |s| == |set x: nat | x in primes :: x|  // 集合大小等于序列去重后的大小
    ensures forall i :: 0 <= i < |primes| ==> primes[i] in s
    {
        s := set x: nat | x in primes :: x;
    }
}

ghost predicate prime(n: nat)
{
    n > 1 && (forall d :: 1 < d < n ==> n % d != 0)
}

method IsPrime(n: nat) returns (p: bool)
{
    if n <= 1 {
        p := false;
        return;
    }
    if n == 2 {
        p := true;
        return;
    }
    p := true;
    var i := 2;
    // 优化：循环到sqrt(n)即可，比n/2效率更高
    while i * i <= n
    invariant 2 <= i <= sqrt(n) + 1
    invariant forall k :: 2 <= k < i ==> n % k != 0
    {
        if n % i == 0 {
            p := false;
            return;  // 找到因数直接返回，无需继续循环
        }
        i := i + 1;
    }
}

关键修正点 #

1. 将CheckPrime方法的modifies s改为modifies this，声明方法会修改当前实例的成员字段
2. 修复IsPrime方法的逻辑错误：
   • 处理n<=1和n==2的边界情况
   • 循环变量从2开始
   • 判断条件改为n % i == 0
   • 优化循环终止条件为i*i <= n，提升效率
3. 完善CreatePrimeBuffer构造函数的后置条件，确保语义正确

内容的提问来源于stack exchange，提问作者felix blasco abril