ContractInvariant method for interface

Question

I am new to contracts I went through documentation of msdn for code contracts

https://msdn.microsoft.com/en-us/library/dd264808(v=vs.110).aspx

I picked the idea of Contract Invariants. However when I add the Invariant method It does not access fields form interface.

[ContractClass(typeof(Account_Contract))]
public interface IAccount
{
    int AccountID { get; }

    string AccountOwner { get; }

    int GetAccountID(); // Our 'internal'unique identifier for this account
}

[ContractClassFor(typeof(IAccount))]
internal abstract class Account_Contract : IAccount
{
    int IAccount.AccountID
    {
        get
        {
            Contract.Ensures(Contract.Result<int>() > 0);
            return default(int);
        }
    }

    string IAccount.AccountOwner
    {
        get
        {
            Contract.Ensures(!String.IsNullOrEmpty(Contract.Result<string>()));
            return default(string);
        }
    }

    int IAccount.GetAccountID()
    {
        Contract.Ensures(Contract.Result<int>() > 0);
        return default(int);
    }
}

It works fine but if I add

Contracts.Requires(AccountID > 0);

VS does not access it. I have also tried

Contracts.Requires(this.AccountID > 0);
Contracts.Requires(IAccount.AccountID > 0);

None working. What is that I'm doing wrong.

Answer 1

You are using explicit implementation of the interface which means that if you want to treat the object as a member of that interface then you need to cast to that first.

So when you want to access AccountID on a instance named myInstance you would need to write ((IAccount)myInstance).AccountId. If you try to access AccountId directly on the class then it will not be recognised.

What this means is that if you need to reference it from within the class for your contracts you should be using ((IAccount)this).AccountId.

The easier way of dealing with this though is to implement the interface implicitly instead and things will be a bit more natural all the way through. To implicitly implement the interface just remove the IAccount. from the beginning of their declarations. For more on implicit and explicit interfaces see C# Interfaces. Implicit implementation versus Explicit implementation .

Answer 2

Your problem is that you are using explicit declaration (as @Chris has comment in his answer), so you have to cast this as IAccount.

I think you should be using implicit declaration (commonly used), in that all methods and props implemented by IAccount must public.

Implicit declaration way:

[ContractClassFor(typeof(IAccount))]
internal abstract class Account_Contract : IAccount
{
    //In order to implement IAccount interface, must be public
    public int AccountID
    {
        get
        {
            Contract.Requires(AccountID > 0);
            return default(int);
        }
    }

    //In order to implement IAccount interface, must be public
    public string AccountOwner
    {
        get
        {
            Contract.Ensures(!String.IsNullOrEmpty(Contract.Result<string>()));
            return default(string);
        }
    }

    //In order to implement IAccount interface, must be public
    public int GetAccountID()
    {
        Contract.Ensures(Contract.Result<int>() > 0);
        return default(int);
    }
}

[ContractClass(typeof(Account_Contract))]
public interface IAccount
{
    int AccountID { get; }

    string AccountOwner { get; }

    int GetAccountID();             ////Our 'internal'unique identifier for this account
}

EDIT: I'm including @Cris 's answer here.

Explicit declaration way:

[ContractClassFor(typeof(IAccount))]
internal abstract class Account_Contract : IAccount
{
    int IAccount.AccountID
    {
        get
        {
            //You must cast this as IAccount
            Contract.Requires(((IAccount)this).AccountID > 0);
            return default(int);
        }
    }

    string IAccount.AccountOwner
    {
        get
        {
            Contract.Ensures(!String.IsNullOrEmpty(Contract.Result<string>()));
            return default(string);
        }
    }

    public int GetAccountID()
    {
        Contract.Ensures(Contract.Result<int>() > 0);
        return default(int);
    }
}