कोड अनुबंध, अगर एक्स <Y और वाई = Z + 1 क्यों है एक्स <Z + 1 साबित नहीं

Question

मैं एक अनुबंध है कि यह करता है:

for (int i = 0; i < delegateParameterTypes.Length; i++) 
{ 
    Contract.Assert(i < delegateParameterTypes.Length); 
    Contract.Assert(delegateParameterTypes.Length == methodParameters.Length + (1)); 
    // Q.E.D. 
    Contract.Assert(i < methodParameters.Length + (1)); 
} 

पहले दो पास विश्लेषण ठीक लेकिन तीसरे कहते हैं कि जोर एक के द्वारा unproven है, एक से बंद? गार्ड पर विचार करें। यह सरल गणित की तरह लगता है। क्या मुझे कुछ याद आ रही है?

स्ट्रिंग एरे और स्थानीय मानों के साथ प्रयास करने से यह ठीक काम करता प्रतीत होता है। किसी भी तरह से तरंग कॉल के साथ क्या करना चाहिए? मैंने intnt को UInt16 पर स्वैप करने का प्रयास किया ताकि यह देखने के लिए कि क्या यह एक लूप में बफर ओवरफ़्लो के कारण है, लेकिन यह भी नहीं था।

Answer 1

हम्म, केवल एक चीज जिसे मैं सोच सकता हूं वह यह है कि स्थैतिक विश्लेषक को इन आवेषणों में समस्या हो रही है। इस पर मेरा अनुसरण करें:

1. आप Contract.Assert(i < delegateParameterTypes.Length); पर कॉल करते हैं। मान लीजिए यह सच है, हम आगे बढ़ते हैं।
2. इस बिंदु पर, स्थिर विश्लेषक को पता नहीं है कि के बारे में कुछ भी Contract.Assert(predicate) और ऊपर चरण 1 के बीच होने वाली किसी भी चीज़ के बीच बदल गया है या नहीं। आप और मुझे नहीं पता कि कुछ भी नहीं हुआ है, लेकिन विश्लेषक नहीं है - इस तथ्य के बावजूद कि कोड की दो पंक्तियां आसन्न हैं (कौन कहने के लिए वहां कुछ धागा साझा राज्य को कहीं छूने वाला नहीं है?)
3. आप अगली कॉल करते हैं: Contract.Assert(delegateParameterTypes.Length == methodParameters.Length + (1)); विश्लेषक यह जांचता है, और यह भी ठीक है।
4. इस बिंदु पर, विश्लेषक पता नहीं कुछ भी बदल गई है कि क्या बारे में delegateParameterTypes या methodParameters --QED, Contract.Assert(i < methodParameters.Length + (1)); अगली पंक्ति के लिए अप्रमाणित का दावा किया है।

फिर, उन चीजों से जुड़े कुछ साझा वैश्विक राज्य हो सकते हैं, और यह स्थिति दो कॉलों के बीच Contract.Assert में बदल सकती थी। याद रखें, आप और मेरे लिए, कोड रैखिक और तुल्यकालिक दिखता है। वास्तविकता काफी अलग हो सकती है या हो सकती है, और स्थिर विश्लेषक Contract.Assert पर लगातार कॉल के बीच उन वस्तुओं की स्थिति के बारे में कोई धारणा नहीं कर सकता है।

क्या काम कर सकते हैं, हालांकि:

int delegateParameterTypesLength = delegateParameterTypes.Length; 
int methodParametersLength = methodParameters.Length + 1; 

for (int i = 0; i < delegateParameterTypesLength; i++) 
{ 
    Contract.Assert(delegateParameterTypesLength == methodParametersLength); 
    // QED 
    Contract.Assert(i < methodParametersLength); 
} 

चर लंबाई आवंटित करके, स्थिर विश्लेषक अब पता कर सकते हैं कि उन मूल्यों for पाश के भीतर बदल नहीं है, या विधि के बाहरी जिसमें वे सौंपा गया अब आप i की तुलना उन मानों से कर रहे हैं जिन्हें बदलने के लिए जाना जाता है। अब, स्थिर विश्लेषक इन मूल्यों की तुलना के बारे में कुछ अनुमान बना सकते हैं और दावाों को साबित करने में सक्षम होना चाहिए।