Dafnyと100人の囚人と電球を証明する

Question

100 prisoners and a lightbulb問題を解決するための標準的な戦略を考えてみましょう。それが失敗した

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でそれを証明するために：ここに私のDafnyでそれをモデル化しようとする試みです。どうして？おそらくループ不変量をさらに強化する必要があるかもしれませんが、どこから始めるのか想像できません。

Answer 1

Hereはこれを行う方法の1つです。

私は、概念的には鍵ループ不変で概念的には重要ではないが、Dafnyの補題を1つ追加しなければならなかった。

何とかさまざまなセットにcountを接続するループ不変式が必要です。さもなければループ後のcount == |P| - 1という事実はそれほど有用ではありません。私はSのカーディナリティにcountを接続

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

を使用することにしました。 （私はSをカウンターによって数えられた囚人のセットと考えています。）ライトが消灯しているときは、countが最新です（つまり、|S| == count）。しかし、ライトが点灯しているときは、カウンターがカウントを更新して更新するのを待っているので、それは1つ遅れています（つまり、|S| == count + 1）。

このループ不変式では、ループの後にI == Pと主張できます。あなたの他のループ不変量の1つでは、すでに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に戻って、ソルバーが関連性がなくても使いすぎていたようで、遅くなってしまったようです。

私たちが誘導によって必要なものを証明することができるので、それは大したことではありませんが、興味深い話です。