与 Dafny 一起证明 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 是 The Counter 统计的囚犯集合。）当灯熄灭时，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 relating cardinality with subsets. (Admittedly, this axiom is about the non-strict subset relation, but by uncommenting this axiom, I was able to get a version of the proof to go through without additional lemmas, so it would be sufficient.) Tracing it back to why the axiom was commented out，即使它不相关，求解器似乎也使用了太多，这减慢了速度。

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

与 Dafny 一起证明 100 个囚犯和一个灯泡

Proving the 100 Prisoners and a lightbulb with Dafny

formal-verification

loop-invariant

dafny