Introducing Code Contracts - Part 2

• Download source - 10.3 KB

Introduction

This article builds on the information presented in my previous article on using Code Contracts in .NET. That article introduced the basics of using Code Contracts, so this article is going to delve further into this technology, and we're going to look at some of the more esoteric and "fun" features available here.

Please read the first article before you read this one, because it is assumed that you know about the pre and postconditions put in place by Code Contracts, and that you are aware of the binary rewriter. 

Object Invariants

Sometimes we may want to have a condition that holds true on an instance of the class. What I mean by this, is that we have a condition (or set of conditions) that must be true following every public method call. Suppose for instance, that you have a requirement that you have a list that cannot be empty (a very heavily contrived example I know), how would we actually do this? Well, we create a private void method that contains only calls to Contract.Invariant, and then mark the method with the ContractInvariantMethod attribute.

[ContractInvariantMethod]
private void TestList()
{
    Contract.Invariant(this.MonitoredList.Count > 0);
}

Now, whenever we call a public method in the class that contains this list, an exception will be thrown if the postcondition indicates that the contract is no longer valid because the invariant indicates that the state of the instance is no longer "good".

You note that I state that this occurs when we call a method, not whenever a public method is executed. There's a very good reason for this; the invariant is checked as a post condition so that you can have a public method in an instance call another public method in the instance without executing the post condition in the second public method. You might do this where the second method temporarily moves the object into an invalid state, but the remaining code in the first method transforms the object back into a valid state.

In the attached sample, we have the following code:

[ContractInvariantMethod]
private void ValidateDocument()
{
    Contract.Invariant(!string.IsNullOrWhiteSpace(this.Filename), 
		"The filename must be set");
    Contract.Invariant(this.Filename.Length < 255, 
		"The filename must be less than 255 characters");
    Contract.Invariant(this.Metadata.Count > 0, "The metadata cannot be empty");
}

public void Change(string filename, List<string> metadata)
{
    Filename = null;
    Metadata.Clear();
    Filename = filename;
    Metadata.AddRange(metadata);
}

As you can see, the Change method does things that would trigger the invariant conditions if we were to call them directly, but because they are in a single public method calling other public methods, the invariant check happens at the end. To see how it does this, we look at what the rewriter produces:

public void Change(string filename, List<string> metadata)
{
    bool flag = this.$evaluatingInvariant$;
    this.$evaluatingInvariant$ = true;
    this.Filename = null;
    this.Metadata.Clear();
    this.Filename = filename;
    this.Metadata.AddRange(metadata);
    this.$evaluatingInvariant$ = flag;
    this.$InvariantMethod$();
}

The invariant method is generated like this:

[CompilerGenerated, ContractInvariantMethod]
protected override void $InvariantMethod$()
{
    if (!this.$evaluatingInvariant$)
    {
        this.$evaluatingInvariant$ = true;
        try
        {
            __ContractsRuntime.Invariant
		(!string.IsNullOrWhiteSpace(this.<filename>k__BackingField), 
                "The filename must be set", "!string.IsNullOrWhiteSpace(this.Filename)");
            __ContractsRuntime.Invariant(this.<filename>k__BackingField.Length < 0xff, 
                "The filename must be less than 255 characters", 
		"this.Filename.Length < 255");
            __ContractsRuntime.Invariant(this.<metadata>k__BackingField.Count > 0, 
                "The metadata cannot be empty", "this.Metadata.Count > 0");
        }
        finally
        {
            this.$evaluatingInvariant$ = false;
        }
    }
}

Caveats

• Don't call a method marked with ContractInvariantMethod directly. The rewriter changes the method name, so you can't call it.
• You can have only one ContractInvariantMethod per class.
• Invariants are not called by IDisposable.Dispose or object finalizers.
• The trick with multiple methods not having their invariant checked doesn't work in a Dispose or Finalizer method. Calling the public method from here will trigger the invariant checking.
• Doing things like directly clearing a list inside an instance, from the calling method, will not trigger the invariant check - this must be done inside the instance.
• Invariants don't work on structs.

Abbreviators

Suppose you have methods in your class that have some of the same parameters, and the same rules need to be applied, it's not very OO to have to copy the same contract elements into each method. Contract abbreviators allow us to add methods which will perform the common validation for us without having to cut and paste code all over the place. Let's extend the Change method above and see what we get.

First of all, let's create the abbreviator method. Create it as a private method, and apply the ContractAbbreviator attribute to it. The bad news; you have to add %programfiles%\Microsoft\Contracts\Languages\ContractAbbreviator.cs to your project to do this - it's not too much of a burden, but it would be nice for it to be a default part of the CC suite.

[ContractAbbreviator]
private void ValidateNameAndMetadata
	(string filename, List<string> metadata, int maxlength)
{
    Contract.Requires(!string.IsNullOrEmpty(filename), "The filename cannot be blank");
    Contract.Requires(metadata != null);
    Contract.Requires(metadata.Count > 0);
    // The postcondition should ensure that the metadata must be less than maxlength
    Contract.Ensures(this.Metadata.Count < maxlength);
}

Now, we need to add a call to this method to our code. Let's choose the Change method and add the call to the abbreviator method.

public void Change(string filename, List<string> metadata)
{
    ValidateNameAndMetadata(filename, metadata, 5);
    Filename = null;
    Metadata.Clear();
    Filename = filename;
    Metadata.AddRange(metadata);
}

Now, if we look at the rewritten code, we see the effect of applying the abbreviator.

[ContractAbbreviator]
private void ValidateNameAndMetadata
	(string filename, List<string> metadata, int maxlength)
{
}

public void Change(string filename, List<string> metadata)
{
    if (__ContractsRuntime.insideContractEvaluation <= 4)
    {
        try
        {
            __ContractsRuntime.insideContractEvaluation++;
            __ContractsRuntime.Requires(!string.IsNullOrEmpty(filename), 
                "The filename cannot be blank", "!string.IsNullOrEmpty(filename)");
            __ContractsRuntime.Requires(metadata != null, null, "metadata != null");
            __ContractsRuntime.Requires(metadata.Count > 0, null, "metadata.Count > 0");
        }
        finally
        {
            __ContractsRuntime.insideContractEvaluation--;
        }
    }
    bool flag = this.$evaluatingInvariant$;
    this.$evaluatingInvariant$ = true;
    this.Filename = null;
    this.Metadata.Clear();
    this.Filename = filename;
    this.Metadata.AddRange(metadata);
    if (__ContractsRuntime.insideContractEvaluation <= 4)
    {
        try
        {
            __ContractsRuntime.insideContractEvaluation++;
            __ContractsRuntime.Ensures(this.Metadata.Count < 5, 
			null, "this.Metadata.Count < maxlength");
        }
        finally
        {
            __ContractsRuntime.insideContractEvaluation--;
        }
    }
    this.$evaluatingInvariant$ = flag;
    this.$InvariantMethod$();
}

It's at this point that the power of the abbreviator becomes apparent. It's automatically applied the pre and postconditions in our method (and conveniently removed any body from the abbreviator method), so we can apply these methods as and where we need them. There are no limits to the number of abbreviators that we can apply in a class.

Contract Quantifiers

Effectively there are two types of contract quantifiers available through Code Contracts. We have Exists and ForAll available to use. With ForAll, we evaluate each element in an enumeration and perform a comparison. In the following example, we are going to check each element in the list to ensure that it is not null or empty.

Contract.Requires(Contract.ForAll(metadata, x => !string.IsNullOrWhiteSpace(x)));

Exists is a predicate applied to each element in a list until a condition is matched, at which point it returns fully. If the predicate fails to find a match, it returns false. The following code sample demonstrates this by ensuring that a document ends with .doc, .jpg, .docs or .xls.

public string[] types = new string[] { ".doc", ".jpg", ".docx", ".xls" };

public void ChangeDocument(string document)
{
    Contract.Requires(Contract.Exists(types, 
        x => string.Compare(x, Path.GetExtension(document), true) == 0));
    this.Filename = document;
} 

Points of Interest

You can't use Contract.Requires<T> when the assembly is set to 'Custom Parameter Validation'. If you want to use this, you need to change the assembly to 'Standard Contract Requires'. You do this through the Code Contracts property page, by setting the Assembly Mode:

When you change the assembly mode to Standard Contract Requires and rebuild the code, the rewritten code looks like this:

public void Change(string filename, List<string> metadata)
{
    bool flag;
    try
    {
        if (__ContractsRuntime.insideContractEvaluation <= 4)
        {
            try
            {
                __ContractsRuntime.insideContractEvaluation++;
                __ContractsRuntime.Requires<argumentoutofrangeexception>
		(!string.IsNullOrEmpty(filename), 
                    "The filename cannot be blank", "!string.IsNullOrEmpty(filename)");
                __ContractsRuntime.Requires(metadata != null, null, "metadata != null");
                __ContractsRuntime.Requires(metadata.Count > 0, 
				null, "metadata.Count > 0");
            }
            finally
            {
                __ContractsRuntime.insideContractEvaluation--;
            }
        }
        flag = this.$evaluatingInvariant$;
        this.$evaluatingInvariant$ = true;
        this.Filename = null;
        this.Metadata.Clear();
        this.Filename = filename;
        this.Metadata.AddRange(metadata);
        this.$evaluatingInvariant$ = flag;
        this.$InvariantMethod$();
    }
    catch (ArgumentOutOfRangeException exception)
    {
        if (__ContractsRuntime.insideContractEvaluation <= 4)
        {
            try
            {
                __ContractsRuntime.insideContractEvaluation++;
                __ContractsRuntime.EnsuresOnThrow(this.Metadata.Count < 5, null, 
                    "this.Metadata.Count < maxlength", exception);
            }
            finally
            {
                __ContractsRuntime.insideContractEvaluation--;
            }
        }
        this.$evaluatingInvariant$ = flag;
        this.$InvariantMethod$();
        throw;
    }
}

It takes a couple of seconds to see the difference between the two types of validation, but the second method wraps the code in a try/catch block to ensure the relevant exceptions are thrown.

Conclusion

As we can see, Code Contracts are very powerful. My big complaint here is that the whole CC experience is not one coherent whole - it requires downloading things, and copying files, all of which is an unnecessary complication. Still, if you can live with these "issues" (and I know I can), Code Contracts offer a valuable tool for your coding arsenal.

History

• 25/08/10 - Initial version