Using Code Contracts to define an immutable interface?

Question

Can I use Code Contracts to define read-only, invariant properties on an interface? I.e. properties which always yield the same value after instantiation?

Answer 1

First a note on terminology in .NET:

• read-only: The interface you happen to have cannot be used to mutate the object or collection
• immutable: Nothing can mutate the object or collection

Now back to your question.

All property getters are implicitly marked as "Pure" in .NET Code Contracts. This means that reading from the getter should never have a visible side-effect.

In a strict sense, if you have an abstract interface with only read-only properties then the whole interface is considered to be read-only.

However, it sounds like what you really want is a way to mark an interface as immutable and have the underlying classes inherit that status. Unfortuantely there is no way to do that, abstract interfaces can only add functionality. And the best that Code Contracts can do is ensure the functionality was added correctly.

Summary

No, it doesn't support that.

Answer 2

Here is a possible solution as a proof of concept. There are various problems with it, not least that all the objects will be kept alive in the cache and we're using an extension method to effectively trick the code contracts framework into allowing us to maintain state, but it does at least demonstrate that this contractual test is possible.

The code below defines various things:

• An interface IRuntimeProperty with a property AlwaysTheSame that returns an integer. We don't care what the value is, but would like it to always return the same thing.
• A static class RuntimePropertyExtensions that defines an extension method IsAlwaysTheSame which uses a cache of previous results from IRuntimeProperty objects.
• A class RuntimePropertyContracts that calls the extension method to check the return value from AlwaysTheSame.
• A class GoodObject that implements AlwaysTheSame in a way we like, so it always returns the same value for a given object.
• A class BadObject that implements AlwaysTheSame in a way we don't like, so consecutive calls return different values.
• A Main method to test the contract.

Here is the code:

using System;
using System.Collections.Generic;
using System.Diagnostics.Contracts;

namespace SameValueCodeContracts
{
    [ContractClass(typeof(RuntimePropertyContracts))]
    interface IRuntimeProperty
    {
        int AlwaysTheSame { get; }
    }

    internal static class RuntimePropertyExtensions
    {
        private static Dictionary<IRuntimeProperty, int> cache = new Dictionary<IRuntimeProperty, int>();

        internal static bool IsAlwaysTheSame(this IRuntimeProperty runtime, int newValue)
        {
            Console.WriteLine("in IsAlwaysTheSame for {0} with {1}", runtime, newValue);
            if (cache.ContainsKey(runtime))
            {
                bool result = cache[runtime] == newValue;
                if (!result)
                {
                    Console.WriteLine("*** expected {0} but got {1}", cache[runtime], newValue);
                }
                return result;
            }
            else
            {
                cache[runtime] = newValue;
                Console.WriteLine("cache now contains {0}", cache.Count);
                return true;
            }
        }
    }

    [ContractClassFor(typeof(IRuntimeProperty))]
    internal class RuntimePropertyContracts : IRuntimeProperty
    {
        public int AlwaysTheSame
        {
            get
            {
                Contract.Ensures(this.IsAlwaysTheSame(Contract.Result<int>()));
                return default(int);
            }
        }
    }

    internal class GoodObject : IRuntimeProperty
    {
        private readonly string name;
        private readonly int myConstantValue = (int)DateTime.Now.Ticks;

        public GoodObject(string name)
        {
            this.name = name;
            Console.WriteLine("{0} initialised with {1}", name, myConstantValue);
        }

        public int AlwaysTheSame
        {
            get
            {
                Console.WriteLine("{0} returning {1}", name, myConstantValue);
                return myConstantValue;
            }
        }
    }

    internal class BadObject : IRuntimeProperty
    {
        private readonly string name;
        private int myVaryingValue;

        public BadObject(string name)
        {
            this.name = name;
            Console.WriteLine("{0} initialised with {1}", name, myVaryingValue);
        }

        public int AlwaysTheSame
        {
            get
            {
                Console.WriteLine("{0} returning {1}", name, myVaryingValue);
                return myVaryingValue++;
            }
        }
    }

    internal class Program
    {
        private static void Main(string[] args)
        {
            int value;

            GoodObject good1 = new GoodObject("good1");
            value = good1.AlwaysTheSame;
            value = good1.AlwaysTheSame;
            Console.WriteLine();

            GoodObject good2 = new GoodObject("good2");
            value = good2.AlwaysTheSame;
            value = good2.AlwaysTheSame;
            Console.WriteLine();

            BadObject bad1 = new BadObject("bad1");
            value = bad1.AlwaysTheSame;
            Console.WriteLine();

            BadObject bad2 = new BadObject("bad2");
            value = bad2.AlwaysTheSame;
            Console.WriteLine();

            try
            {
                value = bad1.AlwaysTheSame;
            }
            catch (Exception e)
            {
                Console.WriteLine("Last call caused an exception: {0}", e.Message);
            }
        }
    }
}

It gives output as follows:

good1 initialised with -2080305989
good1 returning -2080305989
in IsAlwaysTheSame for SameValueCodeContracts.GoodObject with -2080305989
cache now contains 1
good1 returning -2080305989
in IsAlwaysTheSame for SameValueCodeContracts.GoodObject with -2080305989

good2 initialised with -2080245985
good2 returning -2080245985
in IsAlwaysTheSame for SameValueCodeContracts.GoodObject with -2080245985
cache now contains 2
good2 returning -2080245985
in IsAlwaysTheSame for SameValueCodeContracts.GoodObject with -2080245985

bad1 initialised with 0
bad1 returning 0
in IsAlwaysTheSame for SameValueCodeContracts.BadObject with 0
cache now contains 3

bad2 initialised with 0
bad2 returning 0
in IsAlwaysTheSame for SameValueCodeContracts.BadObject with 0
cache now contains 4

bad1 returning 1
in IsAlwaysTheSame for SameValueCodeContracts.BadObject with 1
*** expected 0 but got 1
Last call caused an exception: Postcondition failed: this.IsAlwaysTheSame(Contract.Result())

We can create as many GoodObject instances as we like. Calling AlwaysTheSame on them will always satisfy the contract.

In contrast, when we create BadObject instances, we can call AlwaysTheSame on each one only once; as soon as we call it for the second time, the contract throws an exception because the value being returned is inconsistent with what we got last time.

As I said at the start, I'd be wary of using this approach in production code. But I agree that this is a useful thing to want to specify by contract, and it would be great if there were support for such runtime return-value invariance built into the code contracts framework.