[RESOLVED] Code Contracts - [Pure] Methods

Been a long time since I posted on here!

I am trying to get to grip with code contracts on interfaces. Here's some example code

Code:

---

using System.Diagnostics.Contracts;

namespace Scratch
{

    [ContractClass(typeof(TestContract))]
    public interface ITest
    {
        void Add(int Number);
        void Remove(int Index);
        int Count();
    }


    [ContractClassFor(typeof(ITest))]
    public abstract class TestContract : ITest
    {

        public void Add(int Number)
        {
            throw new System.NotImplementedException();
        }

        public void Remove(int Index)
        {
            Contract.Requires(Index >= 0);
            Contract.Requires(Index <= this.Count());
        }

        [Pure]
        public int Count()
        {
            throw new System.NotImplementedException();
        }

    }

}

---

The problem is that the Code Contracts analyser (or whatever it is called) reports a warning 'CodeContracts: Detected call to method 'Scratch.ITest.Count' without [Pure] in contracts of method 'Scratch.TextContract.Remove(System.Int32)'

I realise that the code contract class is abstract and thus will have no instances, so the question is how do I achieve this?

Thanks,

Y

Hi,

I've never heard of this namespace, so I did some digging. towards the bottom of this link there is a link to the documentation for this namespace. I took a look at the documentation and it looks useful if' you've not got it. I think this might answer some of your problem.

http://www.jarloo.com/code-contracts/

Thanks, Bill. Unfortunately, it doesn't. There seems to be a bug in code contracts not being able to analyse instance methods.

Got it: if you want to use an instance method derived from an interface, you need to do it as a read-only property. Evidently, the Code-Contracts thingy accepts getters as [Pure] and therefore doesn't do a check against a method.

Inferred the answer from http://msdn.microsoft.com/en-us/library/dd264808.aspx