क्या संहिता संविदात्मक जांचकर्ता को अंकगणितीय बाध्य जांचने में सक्षम होना चाहिए?

Question

(इसके अलावा posted on the MSDN forum - लेकिन यह है कि अधिक यातायात, जहाँ तक मैं देख सकता हूँ नहीं मिलता है।)

मैं Assert और Assume का एक उदाहरण प्रदान करने के लिए कोशिश कर रहा हूँ। यहाँ कोड मैं लिया है:

public static int RollDice(Random rng) 
{ 
    Contract.Ensures(Contract.Result<int>() >= 2 && 
        Contract.Result<int>() <= 12); 

    if (rng == null) 
    { 
     rng = new Random(); 
    } 
    Contract.Assert(rng != null); 

    int firstRoll = rng.Next(1, 7); 
    Contract.Assume(firstRoll >= 1 && firstRoll <= 6); 

    int secondRoll = rng.Next(1, 7); 
    Contract.Assume(secondRoll >= 1 && secondRoll <= 6); 

    return firstRoll + secondRoll; 
} 

(एक मौजूदा Random संदर्भ की बजाय एक अशक्त संदर्भ में पारित करने में सक्षम होने के बारे में व्यापार विशुद्ध रूप से निश्चित रूप से शैक्षणिक, है।)

मुझे लगता है कि अगर आशा व्यक्त की थी चेकर को पता था कि firstRoll और secondRoll[1, 6] श्रेणी में प्रत्येक थे, यह काम करने में सक्षम होगा कि राशि [2, 12] सीमा में थी।

क्या यह एक अनुचित उम्मीद है? मुझे एहसास है कि यह एक मुश्किल व्यवसाय है, वास्तव में क्या हो सकता है ... लेकिन मुझे उम्मीद थी कि चेकर पर्याप्त स्मार्ट होगा :)

यदि यह अब समर्थित नहीं है, तो क्या कोई यहां जानता है कि यह समर्थित होने की संभावना है निकट भविष्य में?

संपादित करें: अब मुझे पता चला है कि स्थैतिक चेकर में अंकगणित के लिए बहुत जटिल विकल्प हैं। "उन्नत" टेक्स्ट बॉक्स का उपयोग करके मैं उन्हें विजुअल स्टूडियो से बाहर आज़मा सकता हूं, लेकिन जहां तक ​​मैं कह सकता हूं, उनके बारे में कोई अच्छी व्याख्या नहीं है।

Answer 1

मुझे एमएसडीएन मंच पर एक जवाब मिला है। यह पता चला कि मैं बहुत करीब था। मूल रूप से स्थिर जांचकर्ता बेहतर काम करता है यदि आप "और-ed" अनुबंधों को विभाजित करते हैं। इसलिए, यदि हम इस कोड को बदलते हैं:

public static int RollDice(Random rng) 
{ 
    Contract.Ensures(Contract.Result<int>() >= 2); 
    Contract.Ensures(Contract.Result<int>() <= 12); 

    if (rng == null) 
    { 
     rng = new Random(); 
    } 
    Contract.Assert(rng != null); 

    int firstRoll = rng.Next(1, 7); 
    Contract.Assume(firstRoll >= 1); 
    Contract.Assume(firstRoll <= 6); 
    int secondRoll = rng.Next(1, 7); 
    Contract.Assume(secondRoll >= 1); 
    Contract.Assume(secondRoll <= 6); 

    return firstRoll + secondRoll; 
} 

यह बिना किसी समस्या के काम करता है। इसका मतलब यह भी है कि उदाहरण और भी उपयोगी है, क्योंकि यह बहुत ही महत्वपूर्ण है कि चेकर अलग-अलग अनुबंधों के साथ बेहतर काम करता है।

Answer 2

मुझे एमएस अनुबंध जांचकर्ता उपकरण के बारे में पता नहीं है, लेकिन रेंज विश्लेषण एक मानक स्थैतिक विश्लेषण तकनीक है; यह वाणिज्यिक स्थिर विश्लेषण उपकरण में व्यापक रूप से उपयोग किया जाता है ताकि यह सत्यापित किया जा सके कि सबस्क्रिप्ट अभिव्यक्ति कानूनी हैं।

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