क्या यह स्थिर अनुबंध चेकर में एक बग है?

Question

अगर मैं यह लिख:

public sealed class Foo 
{ 
    private int count; 
    private object owner; 
    private void Bar() 
    { 
     Contract.Requires(count > 0); 
     Contract.Ensures(owner == null || count > 0); 

     if (count == 1) 
      owner = null; 
     --count; 
    } 
} 

स्थिर अनुबंध चेकर गए सभी दावे को साबित कर सकते हैं।

लेकिन अगर मैं इस बजाय लिखें:

public sealed class Foo 
{ 
    private int count; 
    private object owner; 
    private void Bar() 
    { 
     Contract.Requires(count > 0); 
     Contract.Ensures(owner == null || count > 0); 

     --count; 
     if (count == 0) 
      owner = null; 
    } 
} 

उसका दावा है postcondition owner == null || count > 0 अप्रमाणित है।

मुझे लगता है कि मैं साबित कर सकते हैं दूसरा रूप यह postcondition का उल्लंघन नहीं करता:

// { count > 0 } it's required 
--count; 
// { count == 0 || count > 0 } if it was 1, it's now zero, otherwise it's still greater than zero 
if (count == 0) 
{ 
    // { count == 0 } the if condition is true 
    owner = null; 
    // { count == 0 && owner == null } assignment works 
} 
// { count == 0 && owner == null || count != 0 && count > 0 } either the if was entered or not 
// { owner == null || count > 0 } we can assume a weaker postcondition 

कुछ मेरी सबूत के साथ कुछ गलत है?

मैं कोड को Contract.Assert कॉल के रूप में मेरे सबूत में दावे जोड़ा, और मैं निष्कर्ष पर पहुंचा है, तो मैं सिर्फ इस एक जोड़ने के लिए, यह postcondition साबित करने के लिए प्रबंधन करता है कि: अगर मैं,

--count; 
Contract.Assert(count == 0 || count > 0) 
if (count == 0) 
    owner = null; 

लेकिन अब बदल है कि एक "और अधिक प्राकृतिक" जिस तरह से करने के लिए एक ही जोर है, यह विफल रहता है:

--count; 
Contract.Assert(count >= 0) 
if (count == 0) 
    owner = null; 

यह अपेक्षा की जाती है कि उन दो कथनों बराबर थे, लेकिन स्थिर चेकर उन्हें अलग तरह से व्यवहार करता है।

(मैं जिस तरह से VS10 का बीटा 2 का उपयोग कर रहा)

Answer 1

मैं इस बेहद जटिल प्रोवरिंग चीज को पूरी तरह से काम करने वाली स्थिति में होने की उम्मीद नहीं करूँगा क्योंकि यह सिर्फ बीटा है। मुझे लगता है कि यह एक बग है या डेवलपर्स के साथ कम से कम एक बिंदु लायक है, क्योंकि यह स्वचालित रूप से स्थिर जांच के लिए एक बहुत ही सरल बात है।

वैसे भी, चीजों के दिखने से, सुनिश्चितकर्ता मार्कर यह कहने के लिए है कि स्थिर अनुबंध परीक्षक स्थिति सुनिश्चित करने में सक्षम है या नहीं। यह इस बात का तात्पर्य नहीं है कि स्थिति वैध नहीं है, इसका मतलब है कि यह सबूत नहीं मिल सकता है।

मैं उन मामलों के बारे में अधिक चिंतित हूं जहां यह कहता है कि कुछ सुनिश्चित किया गया है जो अमान्य है। कि एक बग के रूप में गिना जाएगा!

Answer 2

चेतावनी: मैं बिल्कुल .net अनुबंध प्रणाली की बारीकियों के बारे में कुछ भी नहीं पता है।

हालांकि, मैं आपको यह बता सकता हूं: यह सचमुच संभव नहीं है (सीएफ। रोकथाम समस्या) दावे के लिए एक पूर्ण समर्थक उत्पन्न करने के लिए जो इस प्रणाली का समर्थन करता है, के रूप में समृद्ध है।

तो: क्या यह एक बग है? सं।

दूसरी तरफ, यह सुझाव देने के लिए व्यावहारिक लगता है कि यह एक आम मामला हो सकता है कि समर्थक के कार्यान्वयनकर्ता अपने सिस्टम में जोड़ना चाहते हैं।