Contracts

I was doing something the other day and I noticed a new namespace that vaguely reminded me of something I looked at a while back.

The namespace in question is System.Diagnostics.Contracts, and the subject I was looking at was Spec# which was a research project for Microsoft. So it looks like some of this is now available in VS2010/.NET4.0.

Though not all of it, looks like you still need to install something extra to get the extra VS2010 Code Contracts tab that Somar talks about on his blog:

I don’t get that using standard VS2010, but hey ho, lets continue our looking at what we can do without installing anything extra.

So I have a really trivial example here where I have a small class:

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;
 
namespace CodeContracts
{
    class Program
    {
        static void Main(string[] args)
        {
            TestClass t = new TestClass();
            t.SomeMethod("one");
            Console.ReadLine();
        }
    }
 
 
    public class TestClass
    {
        private List<string> counts = new List<string>();
 
        public int SomeMethod(string count)
        {
            Contract.Assert(count.Length == 5, "count length must be 5");
            counts.Add(count);
            return counts.Count();
        }
    }
 
}

Note the use of Contract.Assert in there, which generates this at Runtime
.csharpcode, .csharpcode pre
{
font-size: small;
color: black;
font-family: consolas, “Courier New”, courier, monospace;
background-color: #ffffff;
/*white-space: pre;*/
}
.csharpcode pre { margin: 0em; }
.csharpcode .rem { color: #008000; }
.csharpcode .kwrd { color: #0000ff; }
.csharpcode .str { color: #006080; }
.csharpcode .op { color: #0000c0; }
.csharpcode .preproc { color: #cc6633; }
.csharpcode .asp { background-color: #ffff00; }
.csharpcode .html { color: #800000; }
.csharpcode .attr { color: #ff0000; }
.csharpcode .alt
{
background-color: #f4f4f4;
width: 100%;
margin: 0em;
}
.csharpcode .lnum { color: #606060; }

image

Now this is the same as what a lot of us have probably done with small static ArgumentValidator classes etc etc. Not much gain there.

But taking a bigger example (from the example in MSDN), we could have an interface called IArray that we want to implement and we could also have a ContractClassForAttribute and some code contracts on another class that will provide the contracts for a IArray implementation.

// An IArray is an ordered collection of objects.    
[ContractClass(typeof(IArrayContract))]
public interface IArray
{
    // The Item property provides methods to 
    //read and edit entries in the array.
    string this[int index]
    {
        get;
        set;
    }
 
    int Count
    {
        get;
 
    }
 
    // Adds an item to the list.  
    // The return value is the position the new element was inserted in.
    int Add(string value);
 
    // Removes all items from the list.
    void Clear();
 
    // Inserts value into the array at position index.
    // index must be non-negative and less than or equal to the 
    // number of elements in the array.  If index equals the number
    // of items in the array, then value is appended to the end.
    void Insert(int index, string value);
 
 
    // Removes the item at position index.
    void RemoveAt(int index);
}
 
[ContractClassFor(typeof(IArray))]
public abstract class IArrayContract : IArray
{
    int IArray.Add(string value)
    {
        // Returns the index in which an item was inserted.
        Contract.Ensures(Contract.Result<int>() >= -1);
        Contract.Ensures(Contract.Result<int>() < 
            ((IArray)this).Count);
        return default(int);
    }
    string IArray.this[int index]
    {
        get
        {
            Contract.Requires(index >= 0);
            Contract.Requires(index < ((IArray)this).Count);
            return default(string);
        }
        set
        {
            Contract.Requires(index >= 0);
            Contract.Requires(index < ((IArray)this).Count);
        }
    }
    public int Count
    {
        get
        {
            Contract.Requires(Count >= 0);
            Contract.Requires(Count <= ((IArray)this).Count);
            return default(int);
        }
    }
 
    void IArray.Clear()
    {
        Contract.Ensures(((IArray)this).Count == 0);
    }
 
    void IArray.Insert(int index, string value)
    {
        Contract.Requires(index >= 0);
        // For inserting immediately after the end.
        Contract.Requires(index <= ((IArray)this).Count);  
        Contract.Ensures(((IArray)this).Count == 
            Contract.OldValue(((IArray)this).Count) + 1);
    }
 
    void IArray.RemoveAt(int index)
    {
        Contract.Requires(index >= 0);
        Contract.Requires(index < ((IArray)this).Count);
        Contract.Ensures(((IArray)this).Count == 
            Contract.OldValue(((IArray)this).Count) - 1);
    }
}

.csharpcode, .csharpcode pre
{
font-size: small;
color: black;
font-family: consolas, “Courier New”, courier, monospace;
background-color: #ffffff;
/*white-space: pre;*/
}
.csharpcode pre { margin: 0em; }
.csharpcode .rem { color: #008000; }
.csharpcode .kwrd { color: #0000ff; }
.csharpcode .str { color: #006080; }
.csharpcode .op { color: #0000c0; }
.csharpcode .preproc { color: #cc6633; }
.csharpcode .asp { background-color: #ffff00; }
.csharpcode .html { color: #800000; }
.csharpcode .attr { color: #ff0000; }
.csharpcode .alt
{
background-color: #f4f4f4;
width: 100%;
margin: 0em;
}
.csharpcode .lnum { color: #606060; }

So now look at what happens when I create a class that implements IArray.

 

public class TestArrayContractClass : IArray
{
    private List<string> internalItems = new List<string>();
 
    #region IArray Members
 
    public string this[int index]
    {
        get
        {
            return internalItems[index];
        }
        set
        {
            internalItems[index] = value;
        }
    }
 
    public int Count
    {
        get { return internalItems.Count; }
    }
 
    public int Add(string value)
    {
        internalItems.Add(value);
    }
 
    public void Clear()
    {
        internalItems.Clear();
    }
 
    public void Insert(int index, string value)
    {
        internalItems.Insert(index, value);
    }
 
    public void RemoveAt(int index)
    {
        internalItems.RemoveAt(index);
    }
 
    #endregion
}

.csharpcode, .csharpcode pre
{
font-size: small;
color: black;
font-family: consolas, “Courier New”, courier, monospace;
background-color: #ffffff;
/*white-space: pre;*/
}
.csharpcode pre { margin: 0em; }
.csharpcode .rem { color: #008000; }
.csharpcode .kwrd { color: #0000ff; }
.csharpcode .str { color: #006080; }
.csharpcode .op { color: #0000c0; }
.csharpcode .preproc { color: #cc6633; }
.csharpcode .asp { background-color: #ffff00; }
.csharpcode .html { color: #800000; }
.csharpcode .attr { color: #ff0000; }
.csharpcode .alt
{
background-color: #f4f4f4;
width: 100%;
margin: 0em;
}
.csharpcode .lnum { color: #606060; }

See even at design time, I get alerted to the fact that my contract is incorrect, I am not implementing the Add method correctly:

image

So if I try and run this, I will get a problem:

image

So I fix that and run it again, and all is good.

 

And here are some more interesting links on this

Advertisements

9 thoughts on “Contracts

  1. Martin says:

    Isn’t the example a little stupid? You would have got the same error without contracts as not returning a value is always an error in a function…

    • sacha says:

      Yeah it is a stupid example, but I find simple/stupid examples best for illustrating new things. But yeah agreed the example could have been better

  2. meziantou says:

    You say that code contract generates an error message at runtime, but if you want code contracts can just throw an exception as if you do
    throw new Exception();
    You just have to modify an option : Assert on contract failure

  3. Yeah the IArray example is flawed. The error is a compiler error, totally unrelated to contracts.

    Plus, I’m pretty sure that without the code contracts add-on, the separate contract class example would have no runtime effect at all.

    • sacha says:

      Yeah I did have some weirdness, I did end up installing the Contract Spec# MSI and lots of stuff that did not workk (but was available I should point out) started to work. Grrrr. Hear what you are saying about Flawed example, still got people talking about Contracts, so not all bad.

  4. I’m torn between whether or not to use contracts or my old tried and true, runtime-only “ParameterValidation” class. The former feels like the responsible thing to do since its now part of the framework but the fact that so much of it depends upon these extra add-ons to the IDE makes me feel like I can’t trust that the contract code will be enforced.

  5. Nice one man. I like this stuff. I also still use a argument validation class.

    Cheers,
    Daniel

  6. sacha says:

    Daniel

    Yes so do I, time will tell.

    Josh

    Yeah admit the array example could have been better. I am also undecided about this stuff, we shall see

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: