A month or two ago, Visual Studio 2010 and .NET 4.0 betas were released to the developer community. I downloaded these betas and have been using them for a while. VS2010 is nice with a much-needed facelift that doesnít compromise the productivity of the developer. .NET 4.0 introduced F# (fsharp) as a first class language on the CLR. However, one of the most surprising, underrated and exciting features introduced in the new development stack was design by contract (or CodeContract).

Introduction to DBC

DBC is a method of writing and verifying development-level specifications. These specifications come in the form of invariants (in other words, statements that must always be true). These invariants allow for developers to strictly define class interactions, method invocations, mutations, etc. In fact, these definitions are so strict that they can be set to cause compile errors.

Imagine, if you will, a simple function that returns the name of the Person object that it is given (please ignore all bad design issues for this portion, for purposes of demonstration):

public string GetName(Person p)
{
    return p.Name;
}

This simple function, without knowing the context, is an unsafe function. The reason is that it is possible to pass in a null reference to the GetName function which will throw a run-time error of NullReferenceException.

This, being a simple function, is simple to fix. All we need to do is check for a null reference and handle it.

public string GetName(Person p)
{
    if(p == null)
    {
        return "<null>";
    }
    return p.Name;
}

However, this null checking can quickly make code hard to read and takes focus away from the actual function of the code. Another issue is that if you never expect null (e.g. have no requirements for the ìnullî case), then you should probably be throwing an exception. However, that introduces run time bugs. In this circumstance, we would normally sacrifice good exception handling and specification adherence to making the code run-time safe (which is a Good thing, overall).

However, with design by contract we can make a simple method specification that requires non null references to be passed to GetName. This requirement is enforced through static and dynamic model checking of the software:

public string GetName(Person p)
{
    Contract.Requires(p != null);
    return p.Name;
}

So, what does this actually do when you used a null reference call? The model checker will throw a warning (can be set to Error, which I would prefer) stating that the requirements for calling this method have not been met. At this point, the developer would need to look up the code itself or some sort of documentation that would guide her in solving the requirements for calling the method.

Advanced Techniques

This is all a very basic example. Following, I was playing around with some of the .NET 4.0 DBC to create a very familiar data structure. This is a simple tree / node structure with some simple insertion / removal rules. I use a wide breadth of the features provided by CodeContract in order to try to show the power of the framework.

Please note that although I have had some experience with DBC, I am by no means an expert and this is my first foray into the CodeContract framework. If any experts happen to read this and see something wrong, please be my guest to offer criticism.

Tree

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

namespace DBCExample
{
    /// <summary>
    /// Basic Tree/Node data structure to show off Contracts and the
    /// new .NET Framework DBC features.
    /// </summary>
    public class Tree
    {
        public Tree(Node root)
        {
            // Just so that I could show off the invariant, I made root
            // a non-nullable object. While this invariant doesn't hold
            // until after the constructor, invarients are checked from
            // the completion of construction until the object is disposed.
            Contract.Invariant(Root != null);

            Root = root;
        }

        [Pure]
        protected Node Root
        {
            get;
            private set;
        }

        public bool AddNode(Node nodeToAdd)
        {
            // Don't allow null references to be passed to this function
            Contract.Requires(nodeToAdd != null);

            return Root.AddNode(nodeToAdd);
        }

        public void RemoveNode(Node nodeToRemove)
        {
            // For purposes of demonstration, we are requiring that a node
            // be present for it to be removed. In reality, we would want
            // less strict requirements and allow for a non-existent node
            // to be removed.
            Contract.Requires(GetNode(nodeToRemove.Id) != null);
            Contract.Requires(nodeToRemove != null);
            Contract.Ensures(GetNode(nodeToRemove.Id) == null);

            Root.RemoveNode(nodeToRemove);
        }

        // Pure is something that says "Nothing is mutated in this function."
        // This also allows us to use the GetNode statement in the Requires
        // clause of RemoveNode. Nifty, huh?
        [Pure]
        public Node GetNode(int nodeId)
        {
            return Root.GetNode(nodeId);
        }
    }
}

Node

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

namespace DBCExample
{
    /// <summary>
    /// Basic Tree/Node data structure to show off Contracts and the
    /// new .NET Framework DBC features. Node is where this starts to
    /// get really interesting!
    /// </summary>
    public class Node
    {
        private List _children = new List();

        public Node()
        {
            // This shows off the "sanity check" capabilities of the
            // design by contract framework. Without any other DBC code
            // (other than the Pure tag on Descendents) this invariant
            // could run and hold. This is something that is obvious
            // in the domain and if it actually were to occur would
            // be an immediate clue to broken code. Instead, this
            // guards against it at compile time! Neat, huh?
            Contract.Invariant(_children.Count <= Descendents.Count());
            Contract.Invariant(_children != null);
        }

        [Pure]
        public int Id { get; set; }
        [Pure]
        protected Node Parent { get; set; }
        [Pure]
        protected List Descendents
        {
            get
            {
                List descendents = new List();
                descendents.AddRange(_children);
                _children.ForEach(x => descendents.AddRange(x.Descendents));
                return descendents;
            }
        }

        [Pure]
        internal Node GetNode(int nodeId)
        {
            // Essentially an implication, this states that if the Id
            // exists within the children, then the method should return
            // that child. Otherwise, return true (always true if first
            // condition is false).
            Contract.Ensures(
                _children.Exists(x => x.Id == nodeId)
                ? _children.Find(x => x.Id == nodeId) == Contract.Result()
                : true);
            // Same as above but for descendents.
            Contract.Ensures(
                Descendents.Exists(x => x.Id == nodeId)
                ? Descendents.Find(x => x.Id == nodeId) == Contract.Result()
                : true);
            // What the two statements above describe are the two non-null paths.
            // So, all we need to do is describe the null path.
            Contract.Ensures(
                !(Descendents.Exists(x => x.Id == nodeId)
                || _children.Exists(x => x.Id == nodeId))
                ? Contract.Result() == null
                : true);

            foreach (Node n in _children)
            {
                if (n.Id.Equals(nodeId))
                {
                    return n;
                }

                Node possibleNodeFound = n.GetNode(nodeId);
                if (possibleNodeFound != null)
                {
                    return possibleNodeFound;
                }
            }

            return null;
        }

        internal void RemoveNode(Node nodeToRemove)
        {
            Contract.Requires(nodeToRemove != null);

            // This condition should also propogate up to the tree and be written
            // explicitly on the tree itself. However, because _children and Descendents
            // are private and protected, respectively, there is currently no clean
            // method to access these for DBC.
            Contract.Requires(_children.Contains(nodeToRemove)
                || Descendents.Contains(nodeToRemove));

            // Another very powerful example of DBC. This states that if the children
            // contain the node to remove, then the count will be the number of original
            // children, minus one for the removal, plus the descendents of the removed
            // child up to three. Examples:
            //    1 child : 0 descendents => 0 children
            //    2 children : 1 descendent => 2 children
            //    2 children : 3 descendents => 3 children
            Contract.Ensures(Contract.OldValue<list<node>>(_children).Contains(nodeToRemove)
                ? Math.Min(_children.Count - 1 + nodeToRemove.Descendents.Count, 3)
                    == Contract.OldValue<list<node>>(_children).Count
                : false);

            foreach (Node n in _children)
            {
                if (n.Equals(nodeToRemove))
                {
                    _children.Remove(n);

                    // This is an example of a couple of tools available to the DBC programer.
                    // Assert acts as an in-line check of the current context. So, in this,
                    // we are asserting that the count of the children has been reduced by
                    // one.
                    // We also see the Contract.OldValue<t>(T value) appear here. This is a
                    // way of accessing the value of _children before the method started. So,
                    // we can now check before and after conditionals.
                    Contract.Assert(_children.Count - 1
                            == Contract.OldValue<list<node>>(_children).Count);

                    foreach (Node descendent in n.Descendents)
                    {
                        AddNode(descendent);
                    }
                }
                else
                {
                    // The really cool part about this is that we can assume that this method
                    // is pure. We know that this is not correct, but since this is a recursive
                    // method, we have already proven that the assumptions hold with the above
                    // DBC checks. Awesomeness.
                    n.RemoveNode(nodeToRemove);
                }
            }
        }

        internal bool AddNode(Node nodeToAdd)
        {
            Contract.Requires(nodeToAdd != null);

            // There are some interesting constraints that can be added here. However,
            // they really wouldn't demonstrate anything "new." This level of constraints
            // isn't always bad, either, though. Instead, this may be the only constraint
            // that you want to enforce on this method. Using the least amount of constraints
            // to ensure your functionality should be your goal (exceptions to this guideline
            // there are).

            if (_children.Count() < 3)
            {
                _children.Add(nodeToAdd);
                nodeToAdd.Parent = this;
            }
            else
            {
                foreach (Node possibleParentNode in _children)
                {
                    if (possibleParentNode.AddNode(nodeToAdd))
                    {
                        return true;
                    }
                }

                return false;
            }

            return true;
        }

        [Pure]
        public override bool Equals(object obj)
        {
            return Id.Equals(((Node)obj).Id);
        }

        [Pure]
        public override int GetHashCode()
        {
            return base.GetHashCode();
        }
    }
}

Thoughts

Design by contract is a powerful tool. However, like any tool, developers shouldnít rely on just this one. Instead, this is a tool that should be in the toolbox of developers. In fact, this tool is like a torque wrench of tools: a torque wrench is a tool that is absolutely required in some instances but in most cases isnít necessarily or is even wrong to use. I would suggest that DBC be used in very specific circumstances: critical applications, widely used frameworks, complex mathematical algorithms.

Critical applications are applications that need to be 100% correct (or near enough) such as pace makers. Even among critical applications only essential portions may need to be verified for 100% correctness. The reason for such limited usage in applications is because design by contract software could easily take 3 or more times longer to develop than software that doesnít employ the practice. One-hundred percent verified is an expensive process and should only be used in very specific circumstances.

Widely used frameworks (APIs) should use DBC because it promotes developer safety. The model checking of the framework would be of secondary concern to the verification of input requirements. This would allow for developers to know when they are doing something wrong. This could eventually be used to verify correct usage of certain objects such as a FileStream object that was opened but never closed.

Finally, complex mathematical algorithms are difficult to translate to code correctly. However, invariants provide a very mathematical approve to verifying algorithms and thus could aid in the development of these large, complex algorithms.

Dreams

Design by contract and CodeContract are very immature and underdeveloped at this point in time. Research projects have started taking extreme interest in the subject and hopefully further advancements are coming soon. However, I have a few hopes and dreams for CodeContract:

  • Ability to expose private instance methods / variables to an external source for the purposes of model checking (See: JML)
  • Ability to contract interfaces: in fact, this would make much more sense. Instead of contracting the implementations, we should contract the interfaces. This will allow us to swap implementations quickly and easily and still be able to verify that the pre- and post-conditions have been met by the new implementation of the interface.
  • Stand-alone contract runner. The contract runner in Visual Studio essentially runs whenever you build. In addition, the contract warnings / messages / errors appear in the error list (which is good). However, it would be nice to have a separate view that could run the checker on-demand and also aggregate the contract warnings / messages / errors into one place. Also, if that were to occur, possibly link the message and pointer-warning so that multiple errors have distinguishable pointer-warnings.

I apologize for the long post. However, this is a big area to cover in a single blog post and I didnít want to leave anything out. Conclusion: CodeContract is cool but not yet ready for prime time. Perhaps by the time VS2010 ships MSLabs will have something thatís more professional-level rather than research-level.