用Dafny證明100個囚犯和一個燈泡

考慮解決100 prisoners and a lightbulb問題的標準策略。這是我嘗試它Dafny型號：用Dafny證明100個囚犯和一個燈泡

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。爲什麼？我可能需要加強循環不變甚至更進一步，但無法想象從哪裏開始...

來源

2017-06-26 Hugo Sereno Ferreira

Here是一種方法來做到這一點。

我不得不添加一個概念上的關鍵循環不變量和一個不那麼概念上的關鍵 - 但有用的Dafny引理。

您需要一個循環不變式，以某種方式將count連接到各個集合。否則，循環後count == |P| - 1這一事實並不是非常有用。我選擇使用

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

它連接到count的S基數。（我認爲S是櫃檯計數的囚犯）。當燈熄滅時，count是最新的（即|S| == count）。但是當燈亮時，我們正在等待櫃檯注意並更新計數，因此它落後了一位（即|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，即使不相關，解算器似乎也在使用它，這會減慢速度。

它最終不是一個大問題，因爲我們可以通過歸納證明我們需要什麼，但它是一個有趣的消息。

來源

2017-07-29 06:53:47

用Dafny證明100個囚犯和一個燈泡

回答

相關問題