कोड अनुबंध, कुल और कस्टम गणना

Question

मैं सी # 4.0 और कोड अनुबंध का उपयोग कर रहा हूं और मेरे पास अपना स्वयं का कस्टम GameRoomCollection : IEnumerable<GameRoom> है।

मैं यह सुनिश्चित करना चाहता हूं कि GameRoomCollection का कोई भी उदाहरण कभी भी null मान तत्व नहीं रखेगा। हालांकि, मुझे ऐसा करने में सक्षम नहीं लगता है। एक सामान्य नियम बनाने के बजाय, मैंने एक सादा और सरल उदाहरण करने की कोशिश की है। AllGameRoomsGameRoomCollection का एक उदाहरण है।

private void SetupListeners(GameRoom newGameRoom) { 
    Contract.Requires(newGameRoom != null); 
    //... 
} 
private void SetupListeners(Model model) { 
    Contract.Requires(model != null); 
    Contract.Requires(model.AllGameRooms != null); 
    Contract.Assume(Contract.ForAll(model.AllGameRooms, g => g != null)); 
    foreach (GameRoom gameRoom in model.AllGameRooms) 
     SetupListeners(gameRoom);//<= Warning: Code Contracts: Requires unproven: newGameRoom != null 
} 

किसी को भी देख सकते हैं, मैं क्यों साबित नहीं किया, कि gameRoomnull नहीं है?

संपादित करें:

से पहले बार-बार दोहराना या तो काम नहीं करता वस्तु के लिए एक संदर्भ जोड़ना:

IEnumerable<IGameRoom> gameRooms = model.AllGameRooms; 
Contract.Assume(Contract.ForAll(gameRooms, g => g != null)); 
foreach (IGameRoom gameRoom in gameRooms) 
    SetupListeners(gameRoom);//<= Warning: Code Contracts: Requires unproven: newGameRoom != null 

EDIT2:

हालांकि: यदि मैं खेल के कमरे संग्रह प्रकार परिवर्तित एक सरणी में, यह ठीक काम करता है:

IGameRoom[] gameRoomArray = model.AllGameRooms.ToArray(); 
Contract.Assume(Contract.ForAll(gameRoomArray, g => g != null)); 
foreach (IGameRoom gameRoom in gameRoomArray) 
    SetupListeners(gameRoom);//<= NO WARNING 

क्या यह इस तथ्य के कारण है कि आप IEnumerable<T> इंटरफ़ेस के तरीकों के लिए नियम परिभाषित नहीं कर सकते हैं?

EDIT3: क्या समस्या किसी भी तरह this question से संबंधित हो सकती है?

Answer 1

मुझे संदेह है क्योंकि model.AllGameRoomsIEnumerable<GameRoom> देता है जो प्रत्येक संपत्ति के उपयोग पर अलग हो सकता है।

उपयोग करके देखें:

var gameRooms = mode.AllGameRooms; 
Contract.Assume(Contract.ForAll(gameRooms, g => g != null)); 
foreach (IGameRoom gameRoom in gameRooms) 
    SetupListeners(gameRoom);  

Answer 2

मुझे लगता है कि इस GetEnumerator विधि की शुद्धता से कोई लेना देना हो सकता है। PureAttribute

अनुबंध केवल उन तरीकों को स्वीकार करते हैं जिन्हें [शुद्ध] (साइड इफेक्ट फ्री) के रूप में परिभाषित किया जाता है।

कुछ अतिरिक्त जानकारी Code Contracts, look for purity

qoute:

पवित्रता

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

कोड अनुबंध उपकरण वर्तमान में मान लेते हैं कि निम्नलिखित कोड तत्वों शुद्ध कर रहे हैं:

तरीके कि PureAttribute साथ चिह्नित हैं।

PureAttribute के साथ चिह्नित किए गए प्रकार (विशेषता सभी प्रकार के तरीकों पर लागू होती है)।

संपत्ति एक्सेसर्स प्राप्त करती है।

ऑपरेटर्स (स्थिर तरीकों जिनके नाम "सेशन" से शुरू , और कहा कि एक या दो पैरामीटर और एक गैर शून्य वापसी प्रकार है)।

कोई भी तरीका जिसका पूरी तरह से योग्य नाम साथ "System.Diagnostics.Contracts.Contract" शुरू होता है, "System.String", "System.IO.Path", या "System.Type"।

कोई भी आमंत्रित प्रतिनिधि, बशर्ते प्रतिनिधि प्रकार को PureAttribute के साथ को जिम्मेदार ठहराया गया है। प्रतिनिधि प्रकार सिस्टम। प्रमाणीकरण और सिस्टम। सामग्रियों को शुद्ध माना जाता है।