Example: Controlling randomizer using code contracts

One cool addition to Visual Studio 2010 is support for code contracts. Code contracts make sure that all conditions under what method is supposed to run correctly are met. Those who are familiar with unit tests will find code contracts easy to use. In this posting I will show you simple example about static contract checking (example solution is included).

To try out code contracts you need at least Visual Studio 2010 Standard Edition. Also you need code contracts package. You can download package from DevLabs Code Contracts page.

NB! Speakers, you can use the example solution in your presentations as long as you mention me and this blog in your sessions. Solution has readme.txt file that gives you steps to go through when presenting solution in sessions. This blog posting is companion posting for Visual Studio solution referred below.

As an example let’s look at the following class.


public class Randomizer

{

    public static int GetRandomFromRange(int min, int max)

    {

        var rnd = new Random();

        return rnd.Next(min, max);

    }

 

    public static int GetRandomFromRangeContracted(int min, int max)

    {

        Contract.Requires(min < max, "Min must be less than max");

 

        var rnd = new Random();

        return rnd.Next(min, max);

    }

}


GetRandomFromRange() method returns results without any checking. GetRandomFromRangeContracted() uses one code contract that makes sure that minimum value is less than maximum value. Now let’s run the following code.


class Program

{

    static void Main(string[] args)

    {

        var random1 = Randomizer.GetRandomFromRange(0, 9);

        Console.WriteLine("Random 1: " + random1);

 

        var random2 = Randomizer.GetRandomFromRange(1, 1);

        Console.WriteLine("Random 2: " + random2);

 

        var random3 = Randomizer.GetRandomFromRangeContracted(5, 5);

        Console.WriteLine("Random 3: " + random3);

 

        Console.WriteLine(" ");

        Console.WriteLine("Press any key to exit ...");

        Console.ReadKey();

    }
}


As we have not turned on support for code contracts the code runs without any problems and we get no warnings by Visual Studio that something is wrong.

Now let’s turn on static checking for code contracts. As you can see then code still compiles without any errors but Visual Studio warns you about possible problems with contracts.

Visual Studio 2010: Code contracts settings
Click on image to see it at original size. 

When we open Error list and run our application we get the following output to errors list. Note that these messages are not shown immediately. There is little delay between application starting and appearance of these messages. So wait couple of seconds before going out of your mind.

Visual Studio 2010: Warnings by code contracts
Click on image to see it at original size. 

If you look at these warnings you can see that warnings show you illegal calls and also contracts against what they are going. Third warning points to GetRandomFromRange() method and shows that there should be also problem that can be detected by contract.

Download

vs2010-solution Code Contracts example
VS2010 solution | 30KB

No Comments