formal-verification - 用达夫尼证明 100 名囚犯和一个灯泡

Question

考虑解决 100 prisoners and a lightbulb 的标准策略问题。这是我在 Dafny 中对其进行建模的尝试:

method strategy<T>(P: set<T>, Special: T) returns (count: int)
  requires |P| > 1 && Special in P
  ensures count == (|P| - 1)
  decreases *
{
  count := 0;
  var I := {};
  var S := {};
  var switch := false;

  while (count < (|P|-1)) 
    invariant count <= (|P|-1) 
    invariant count > 0 ==> Special in I
    invariant Special !in S && S < P && S <= I && I <= P 
    decreases *
  { 
    var c :| c in P;
    I := I + {c};

    if c == Special {
      if switch == true {
        switch := false;
        count := count + 1;
      }
    } else {
      if c !in S && switch == false {
        S := S + {c};
        switch := true;
      }
    }
  }  

  assert(I == P);  
}

然而，它最终无法证明 I == P .为什么？我可能需要进一步加强循环不变性，但无法想象从哪里开始......

Answer 1

Here 是一种方法。

我不得不添加一个概念上的关键循环不变式和一个概念上不那么关键但对 Dafny 有帮助的引理。

您需要一个循环不变量，以某种方式将 count 连接到各种集合。否则循环后的 count == |P| - 1 不是很有用。我选择使用

if switch then |S| == count + 1 else |S| == count

它将 count 连接到 S 的基数。 (我认为 S 是计数器计数的囚犯集合。)当灯熄灭时， count 是最新的(即 |S| == count )。但是当灯亮时，我们正在等待 The Counter 注意到并更新计数，因此它落后了一个(即 |S| == count + 1 )。

有了这个循环不变性，我们现在可以论证循环之后的 I == P。通过您的其他循环不变量之一，我们已经知道 I <= P 。所以证明 P <= I 就足够了。假设改为 I < P 。然后我们有 S < I < P 。但是根据循环退出条件，我们也有 |S| == |P| - 1 。这是不可能的。

唯一的问题是，Dafny 不能直接将子集关系与基数关系联系起来，所以我们必须帮助它。我证明了一个引理 CardinalitySubset ，给定集合 A 和 B 使得 A < B ，它遵循 |A| < |B| 。证明通过对 B 进行归纳，并且相对简单。用相关的集合调用它完成了主要的证明。

顺便说一句，我研究了为什么 Dafny 不直接将子集关系连接到基数关系。在 Dafny 关于集合的公理中，我发现了 commented out axiom 将基数与子集相关联。 (诚​​然，这个公理是关于非严格子集关系，但是通过取消注释这个公理，我能够得到一个版本的证明，无需额外的引理就可以通过，所以这就足够了。)将其追溯到 why the axiom was commented out ，即使它不相关，求解器似乎也过度使用它，这会减慢速度。

它最终不是什么大问题，因为我们可以通过归纳证明我们需要什么，但这是一个有趣的花絮。