Click here to Skip to main content
Click here to Skip to main content

Introducing Code Contracts - Part 2

, 25 Aug 2010 CPOL
Rate this:
Please Sign up or sign in to vote.
Using Code Contracts to make elegant code

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:

Assembly mode setting showing types

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

License

This article, along with any associated source code and files, is licensed under The Code Project Open License (CPOL)

Share

About the Author

Pete O'Hanlon
CEO
United Kingdom United Kingdom
A developer for over 30 years, I've been lucky enough to write articles and applications for Code Project as well as the Intel Ultimate Coder - Going Perceptual challenge. I live in the North East of England with 2 wonderful daughters and a wonderful wife.
 
I am not the Stig, but I do wish I had Lotus Tuned Suspension.
Follow on   Twitter   Google+

Comments and Discussions

 
QuestionInvariant and ContractClassFor PinmemberDavL816-Jan-14 13:44 
NewsContractAbbreviatorAttribute PinmemberNaecky23-Jul-12 0:38 
QuestionThanks for sharing PinmemberHenning Dieterichs30-May-12 12:55 
At first: Thanks for sharing your knowledge!
 
But I've still a few questions:
Using this code-contract library prevents accessing a class instance from different threads, as "__ContractsRuntime.insideContractEvaluation--" does not look as being thread safe, isn't it?
And for which purpose the insideContractEvaluation variable is used (what means the magical number 4)?
 
And what is the difference between list.All(predicate) and Contract.ForAll(list, predicate) or between list.Any(predicate) and Contract.Exists(list, predicate)?
 
Can I say:
Precondition fails -> the user or the software could caused the malfunction;
Postcondition, Invariant contract fails -> the software contains definitely a bug?
 
At which level I have to check contracts?
That properties are set properly, Id = id?
Consider the following example:
public void Initialize(string name)
{
  Name = name;
  if (Name != name) throw new WhatEverException();
}
 
That calculations are correct (Crc = Checksum(Data))?
In which way post-contracts are different from the stuff actually done in the implementation (if you want to check the result you have to go the way again [I hope you understand my problem])?
How deep preconditions have (or should) to check the correctness of values?
Should the format of the values be checked? The range? The plausibility? Should credentials be verified in the preconditions?
 
Should the preconditions be so precise, that exceptions, which are thrown (if so), can be only caused by real bugs?
 
Besides, the method name "ValidateNameAndMetadata" sounds (for me) like validating values, so "ValidateNameAndMetadata(filename, metadata, 5);" would validate the values (and throw, if necessary, an exception), which is not true (this strengthened my confusion in your first part).
In my opinion something like "ImportContractsForNameAndMetadata" would fit better.
 
Quote:
You might do this where the second method temporarily moves the object into an invalid state

This shouldn't happen, as the second method is public, too (extracted from the sentence before).
If the second method is public, you can call it from outside, so if the (public) method temporarily moves the object into an invalid state, this would violate the invariant contract (=> bug in the software).
So the only reason I can see for using the flag "this.$evaluatingInvariant$" is to increase the performance.
 

Reason for my vote of 4 (but tending towards 3):
Some of your explanations are quite cumbersome (I had to read some passages more than twice to understand them), and it is not easy to follow...
And (in my opinion) for two articles the problematic of contracts is not pointed out enough.
Nevertheless, good job Wink | ;)
If you find spelling- or grammer-mistakes, please let me know, so that I can correct them (at least for me) - english is not my first language...

AnswerRe: Thanks for sharing PinprotectorPete O'Hanlon30-May-12 14:25 
GeneralMy vote of 5 PinmemberMario Majcica24-May-12 6:06 
GeneralRe: My vote of 5 PinmemberMario Majcica24-May-12 6:07 
GeneralMy vote of 5 PinmemberMario Majcica13-Feb-12 2:28 
GeneralUser friendly messages PinmemberRugbyLeague30-Sep-10 7:04 
GeneralRe: User friendly messages PinmvpPete O'Hanlon6-Oct-10 0:38 
GeneralMy vote of 5 PinmemberEric Xue (brokensnow)6-Sep-10 14:12 
GeneralRe: My vote of 5 PinmvpPete O'Hanlon7-Sep-10 5:50 
GeneralRe: My vote of 5 PinmemberEric Xue (brokensnow)7-Sep-10 11:37 
GeneralMy vote of 5 PinmemberMarcelo Ricardo de Oliveira1-Sep-10 5:50 
GeneralRe: My vote of 5 PinmvpPete O'Hanlon1-Sep-10 5:55 
GeneralLooks nice Pinmemberkul.pirate1-Sep-10 4:06 
GeneralRe: Looks nice PinmvpPete O'Hanlon1-Sep-10 4:13 
GeneralPretty good man, I had researched up to your 1st article myself but... PinmvpSacha Barber27-Aug-10 0:58 
GeneralRe: Pretty good man, I had researched up to your 1st article myself but... PinmvpPete O'Hanlon27-Aug-10 1:21 
GeneralRe: Pretty good man, I had researched up to your 1st article myself but... PinmvpSacha Barber27-Aug-10 1:24 
GeneralMy vote of 5 PinmemberNuri Ismail26-Aug-10 21:41 
GeneralRe: My vote of 5 PinmvpPete O'Hanlon26-Aug-10 22:56 
GeneralMy vote of 5 PinmemberYuriy Levytskyy26-Aug-10 5:52 
GeneralRe: My vote of 5 PinmvpPete O'Hanlon26-Aug-10 5:53 
GeneralMy vote of 5 PinmentorKunalChowdhury26-Aug-10 2:36 
GeneralRe: My vote of 5 PinmvpPete O'Hanlon26-Aug-10 2:57 
GeneralThanks PinmemberScruffyDuck26-Aug-10 0:18 
GeneralRe: Thanks PinmvpPete O'Hanlon26-Aug-10 0:23 

General General    News News    Suggestion Suggestion    Question Question    Bug Bug    Answer Answer    Joke Joke    Rant Rant    Admin Admin   

Use Ctrl+Left/Right to switch messages, Ctrl+Up/Down to switch threads, Ctrl+Shift+Left/Right to switch pages.

| Advertise | Privacy | Terms of Use | Mobile
Web02 | 2.8.141216.1 | Last Updated 25 Aug 2010
Article Copyright 2010 by Pete O'Hanlon
Everything else Copyright © CodeProject, 1999-2014
Layout: fixed | fluid