Can an Invariant method [ContractInvariantMethod] work inside an Interface Contract?

I'm creating an Interface Contract as described in § 2.8 Interface Contracts of Feb 4, 2011 Code Contracts User Manual (PDF). This is not a problem.

Additionally I want to mix an Object Invariant (see § 4.2 ContractInvariantMethod) into the same Interface Contract. This is a problem. I cannot find examples of Object Invariants being used on Interface Contracts.

I tried adding an Object Invariant to the Interface Contract seen in the following partial code snippet. It compiles. At runtime it doesn't raise any errors, however it doesn't appear to do anything positive (i.e. be invoked) either.

/* Note: The intention of this snippet is to cause the data implementation
 * to fail if开发者_Python百科 it is not initalized before its public data access methods are called. 
 */
[ContractClassFor(typeof(IDataProxy))]
abstract class IDataProxyContract : IDataProxy
{
    [ContractInvariantMethod]
    private void ObjectInvariant()
    {
        Contract.Invariant(IsInited == true, "Instance not initialized.");
    }

I can't find documentation that specifically addresses this scenario or refutes it.

At this point I'm unsure if I'm missing a step to make it work, or if Code Contract technology ignores the Object Invariant in this context altogether. I would like to make it work. Does anybody know the answer?

Apparently the answer is in the DevLabs forum answered by Manuel Fahndrich, Microsoft (MSFT):

Object invariants are not supported on interfaces at the moment. I can see why they might be handy though.

Full context and code sample here...

They are off by default.

My guess is that the contracts are not enabled by the compiler options, so they don't get weaved into the code.

the solution is to download this package from devlabs

• http://msdn.microsoft.com/en-us/devlabs/dd491992

after you install it, go to the project properties, and you'll see another tab.

then, you can enable an option: "Perform runtime contract checking: full"

Invariants provide a mechanism for constraining the internal state of an object.

They are seen as implementation details which is why they are implemented inside a private method. Interfaces obviously have no concept of state (even properties are just syntactic sugar for methods), and consequently cannot have invariants. In their most primitive use, invariants are used on fields. However, the concept of automatic properties has obviously blurred this line, leading to confusion in this case.

I agree there should be a more concise way of contracting properties, simply because your pre and post conditions are invariably going to be the same.