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.

Where and what is your problem? did you try this `Contracts.Requires(Contract.Result() > 0);`? — Facundo La Rocca, Jan 06 '17 at 13:30
I want make one certain member of IAccount as invariant. Like, Contract.Invariant(IAccount.AccountID > 0); — Usama Aslam, Jan 06 '17 at 13:41

score 2 · Accepted Answer · edited May 23 '17 at 12:24

2

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 .

edited May 23 '17 at 12:24

Community

1
1

answered Jan 06 '17 at 14:02

Chris

27,210
6
71
92

I think his problem is that props are not public, tecnically the interface is not implemented. – Facundo La Rocca Jan 06 '17 at 14:05
And also you are right, he is using explicit declaration when he should be using implicit way. – Facundo La Rocca Jan 06 '17 at 14:07
@FacundoLaRocca: An explicitly implemented interface is by definition public. And in fact one step further it is actually not allowed to put the public modifier on an explicitly implemented member. – Chris Jan 06 '17 at 14:11
You are correct I figured that out myself later. Implementation has to be explicit as am doing it for code contracts. – Usama Aslam Jan 06 '17 at 15:15
@UsamaAslam: Cool. I haven't used code contracts much so not sure on the ins and outs of them. Am more solid on interface implementations. Glad you've got it sorted now though. :) – Chris Jan 06 '17 at 15:17

Facundo La Rocca · Answer 2 · 2017-01-06T15:21:56.870

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);
    }
}

Doing this does not inherit AccountID from IAccount. Also I do not have a problem there. Problem appears when I try to access members of IAccount in Contracts.ensure or Invariants — Usama Aslam, Jan 06 '17 at 13:49
@UsamaAslam: This is implementing the AccountID implicitly. See http://stackoverflow.com/questions/143405/c-sharp-interfaces-implicit-implementation-versus-explicit-implementation for explanation of the difference between explicit and implicit implementation. — Chris, Jan 06 '17 at 13:54
You're first line is still wrong: "he problem is that your properties are not public, so they are not implemented.". As I commented on my post when it came up explicitly implemented interface members are automatically public and it is actually illegal to put the public keyword on them. So the interface is implemented in a valid way (though maybe not the best way). — Chris, Jan 06 '17 at 15:12

ContractInvariant method for interface

2 Answers2

Implicit declaration way:

Explicit declaration way: