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 एक तरह से यह करने के लिए है।

मैं एक धारणात्मक कुंजी पाश अपरिवर्तनीय और एक नहीं-तो-धारणात्मक कुंजी बल्कि उपयोगी करने वाली Dafny लेम्मा जोड़ने के लिए किया था।

आप एक पाश अपरिवर्तनीय किसी भी तरह विभिन्न सेट करने के लिए count जोड़ता है की जरूरत है। अन्यथा यह तथ्य कि count == |P| - 1 लूप के बाद बहुत उपयोगी नहीं है। मैं

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

जो S की प्रमुखता को count जोड़ता है का उपयोग करने के लिए चुना है। (मुझे 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 पर प्रेरण से चला जाता है, और अपेक्षाकृत सरल है। प्रासंगिक सेट के साथ इसे कॉल करने से मुख्य सबूत खत्म हो जाता है।

---

एक तरफ, मैंने थोड़ा सा देखा कि क्यों डेफी सीधे कार्डिनिटी रिश्तों को सबसेट रिश्तों को कनेक्ट नहीं करता है। सेट के बारे में डेफनी के सिद्धांतों में, मुझे commented out axiom सबसेट के साथ कार्डिनलिटी से संबंधित मिला। (माना जाता है कि यह वसंत गैर-सख्त सबसेट संबंध के बारे में है, लेकिन इस वसंत को अपरिवर्तित करके, मैं बिना किसी अतिरिक्त लेमा के बिना सबूत का एक संस्करण प्राप्त करने में सक्षम था, इसलिए यह पर्याप्त होगा।) इसे वापस why the axiom was commented out पर ट्रेस करना, ऐसा लगता है जैसे सॉल्वर इसे बहुत अधिक इस्तेमाल कर रहा था, भले ही यह प्रासंगिक न हो, जिससे चीजों को धीमा कर दिया गया।

यह एक बड़ा सौदा नहीं है क्योंकि हम साबित कर सकते हैं कि हमें प्रेरण से क्या चाहिए, लेकिन यह एक दिलचस्प बात है।