In this fourth segment concerning Microsoft Code Contracts, we're going to look at object invariants. Before we begin, I'll define what an invariant is. With the rising popularity of functional programming languages these days, you might suppose that invariance is a synonym for immutability. Something that doesn't vary could be described as not mutating or not changing, right? But in computer science, that's not what invariant means.

In this realm, an invariant is simply a set of conditions that must hold true both before and after a set of operations. It doesn't mean that things cannot change. It simply means that the set of tests that hold true before a method is called must also hold true after the method runs. To demonstrate this concept, imagine a class called DiscountPercentage that describes the percentage by which the price of the items in a shopping cart may be reduced:

using System;

public class DiscountPercentage
{
    private const float _max = 25.0f;

    private float _value = 0.0f;

    public float Value
    {
        get { return _value; }
        set { _value = value; }
    }
}

This code looks OK but it's not enforcing the _max constant as the upper bound of the _value variable. Let's use an object invariant method to do that. Here's the entire class definition again with a new method not so surreptitiously named Invariants added in.

using System;
using System.Diagnostics.Contracts;

public class DiscountPercentage
{
    private const float _max = 25.0f;

    private float _value = 0.0f;

    public float Value
    {
        get { return _value; }
        set { _value = value; }
    }

    [ContractInvariantMethod]
    private void Invariants()
    {
        Contract.Invariant(_value >= 0.0f);
        Contract.Invariant(_value <= _max);
    }
}

Let me make a few observations about the new Invariants method added to the DiscountPercentage class:

  1. It is marked private: a requirement. If you try to mark it with any other access level modifier, you'll get a warning from the static checker. It will still work at runtime if you have the runtime checker enabled but it's a bad idea to expose this method. And you should never call it directly. Code Contracts will call it automatically at runtime after each public method is invoked if you have the runtime checker enabled.
  2. It returns void: also a requirement.
  3. The name of the method itself is not meaningful. I could have called the object invariant method Jabberwocky (or something else equally meaningless) had I chosen to.
  4. The method is marked with the [ContractInvariantMethod] attribute: also a requirement. This is how Code Contracts knows that this is the special object invariant method containing all of the conditions that must hold true after each public method.
  5. You may mark more than one method in your class as a [ContractInvariantMethod] but you'll probably want to keep it simple, defining a single object invariant method per class.
  6. Inside the invariant method, the only statements that appear are calls to the Contract.Invariant method, passing the conditions that must hold true.

If you build the code shown above, enabling the Code Contracts static checker, you'll get an interesting warning from the static checker:

Warnings emitted by the static checker after the object invariant method is added to the class.

There's that word "unproven" again. We saw that term in Part 2 of this series when I had defined pre-conditions that my method caller didn't meet, remember? But in this case, the message says "invariant unproven" instead of "requires unproven". Double clicking on the first warning will highlight the curly braces for the set mutator of the Value property. Assigning any unchecked value passed to the mutator could put the DiscountPercentage object into an invalid state. The static checker knows this because of the invariant method that was defined. I can add some pre-conditions to the Value property mutator to satisfy the static checker:

public float Value
{
    get { return _value; }
    set
    {
        if (value < 0.0f)
            throw new ArgumentOutOfRangeException();
        if (value > _max)
            throw new ArgumentOutOfRangeException();
        Contract.EndContractBlock();

        _value = value;
    }
}

A rebuild now shows that all the assertions have been proven. Personally, I think this is one of the most useful features of Code Contracts. By defining an invariant method, you are essentially saying, "These things must always be true." After defining the invariant, Code Contracts will make you prove that those conditions are indeed true. When I refactor a legacy project to add Code Contracts, this is the very first thing I do. I look at what the requirements are, implicit or explicit. I ask, "What must always be true?" Then I write an object invariant method for all of those conditions. The warnings on the next build will tell me where I need pre- and post-conditions to ensure the truth of the invariant. That's just fantastic.

If you do object mocking as part of your testing methodology, you'll recognize a pattern here. I am a fan of the NMock framework for .NET. When I write mocks into my tests, I'm essentially wiring up implementations of interfaces based on the known requirements. With NMock, I use the Expect() method to set up some expectations and at the end of a test, I commonly call a method known as VerifyAllExpectationsHaveBeenMet() to, as the name implies, verify that all the expectations have been met. Sound familiar?

The great thing about mocking as part of a Test Driven Development process is that it forces me to think about the requirements in great detail. Mocking allows me do this before I write any real code. With mock objects I can isolate specific behaviors that aren't encumbered with the complexities of production code, making my tests highly-focused and replay-friendly. The mock objects become a form of documentation. Writing object invariants for Code Contracts puts me into a similar mindset. I must focus on what it means for my class to be in a valid state and that forces me to understand the requirements. Then I document those requirements in the object invariant method. The difference, of course, is that my mocked up interfaces do me little good outside of my testing framework. However, the contracts on my code, assisted by the static checker, become a living, breathing part of every build, generating warnings that can be promoted to errors. And if I enable the runtime checker, those very same requirements graduate to become a living, breathing part of the application itself.

To finish this concept of object invariants, let's suppose that a developer receives a requirement to add an AdjustValue method to the DiscountPercentage class in the future to increase or decrease the value of the discount percentage by an offset. A novice, this developer, he's tempted to write something simple like:

public float AdjustValue(float adjustment)
{
    return _value += adjustment;
}

But the static checker will bark at this code, telling him that the it potentially violates the invariant. Specifically, the invariant is unproven by the new code so he's forced to deal with it. The requirements, now documented and enforced by the invariant, will not allow blatantly sloppy code like this to be added to the project. Eventually, after wrestling with the warnings, the novice developer will realize that he has to write something like this instead:

public float AdjustValue(float adjustment)
{
    float newValue = _value + adjustment;
    if (newValue < 0.0f || newValue > _max)
        throw new ApplicationException();
    return _value = newValue;
}

And, of course, the static checker breaths a sigh of relief at these changes, telling the eager, young developer that all the assertions in the code have been satisfied. That's all for this post. Hopefully you're motivated by what you read here to go refactor a legacy project, inserting an object invariant method into an existing class and following the lead of the Code Contracts static checker to shore up the documentations and assumptions throughout the code base. Let me know how that goes. Enjoy.

This blog post is part of a series concerning Microsoft Code Contracts. For a complete series directory, please refer to the following list. Articles without a link will be published as they become available.