17

考虑解决100 名囚犯和一个灯泡问题的标准策略。这是我在 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。为什么?我可能需要进一步加强循环不变量,但无法想象从哪里开始......

4

1 回答 1

4

是一种方法。

我必须添加一个概念上的关键循环不变量和一个在概念上不太重要但对 Dafny 引理有帮助的引理。

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

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

count与 的基数有关S。(我认为是SThe Counter 统计的一组囚犯。)当灯熄灭时,count它是最新的(即|S| == count)。但是当灯亮时,我们正在等待计数器通知并更新计数,所以它落后了(即|S| == count + 1)。

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

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


顺便说一句,我稍微研究了为什么 Dafny 不直接将子集关系与基数关系联系起来。在 Dafny 关于集合的公理中,我发现了一个将基数与子集相关的已注释掉的公理。(诚​​然,这个公理是关于非严格子集关系的,但是通过取消注释这个公理,我能够在没有额外引理的情况下获得一个要通过的证明版本,所以这就足够了。)追溯到为什么axiom 被注释掉了,似乎求解器使用了太多,即使它不相关,这会减慢速度。

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

于 2017-07-29T06:53:47.177 回答