如何验证埃拉托斯特尼筛法代码正确性？求证明方案

需求与问题 #

我需要编写可验证的埃拉托斯特尼筛法（sieve of Eratosthenes）代码，确保该方法仅返回质数。尝试为代码添加不变式与保证条件，但无法通过验证器完成证明。

算法与证明思路 #

算法逻辑 #

采用带优化的埃氏筛法：

• 使用大小为n+1的bool数组（索引范围0到n），True表示对应索引为质数，False表示合数
• 遍历从2到√n的数字，若当前数标记为质数，则将其右侧所有倍数（从该质数的平方开始）标记为合数
• 目前至少希望先完成无优化版本的验证

证明思路 #

• 索引i从左到右遍历2到√n：
  • 若遇到sieve[i] == true，则移除数组中所有大于i且是i倍数的数
  • 若遇到sieve[i] == false，则存在k < i使得i % k == 0（初始数组全为True）
  • 若sieve[i] == true，则对所有k < i，i % k != 0，即i是质数

但上述思路下的简单断言无法成立，需要明确修正方法或更简洁的证明路径。

现有代码 #

质数判断谓词 #

predicate is_prime(k: nat)    
{
    k > 1 && forall d :: 2 <= d < k ==> k % d != 0
}

筛法实现方法 #

method EratosthenesSieve(n: nat) returns (primes: set<nat>)        
    requires n > 2    
    //[1] 需要证明：返回的集合中所有元素都是质数
    ensures forall k :: k in primes ==> is_prime(k)
    //[2] 需要证明：2到n之间的所有质数都在返回集合中
    ensures forall k :: 2 <= k <= n && is_prime(k) ==> k in primes
{
    var sieve: array<bool> := new bool[n+1];
    forall i:nat | 2 <= i < n { sieve[i] := true; }    

    var i: nat := 2;
    assert forall i:nat :: 2 <= i < n ==> sieve[i] == true;
    while i * i < n
        invariant 2 <= i < n < sieve.Length        
        decreases n - i
    {
        if sieve[i] {            
            forall j:nat | (i * i <= j < n) && (j % i == 0) { sieve[i] := false; }    
            //[3] 此处断言无法通过验证
            assert forall j:nat :: (i * i <= j < n) && (j % i == 0) ==> sieve[j] == false;
        }
        i := i + 1;
    }
    primes := {}; 
    for i := 2 to n {
        if sieve[i] {
            primes := primes + {i};
        }
    }    
}

内容的提问来源于stack exchange，提问作者Neocron