Code Contracts in .NET

Visual Studio 2010 beta 1 ships with a new feature called Code Contracts. This is the result of a Microsoft Research project. They allow you to specify coding assumptions in .NET programs. These assumptions can be pre-condition, post-condition and object invariants. However, this new feature can also be used in Visual Studio 2008, except that one needs a separate download, from DevLabs.

The same download is actually necessary for Visual Studio 2010, because beta 1 does not ship with the tools that perform the static or runtime checks on the contracts. It's likely that the final release will include these tools, but one can start writing code contracts even without the tools, and have the code compiling. The contracts code is available in namespace System.Diagnostics.Contracts.

When you download and install the tools, an additional property page is added to your .NET properties. It's called Code Contracts and allows you to specify runtime and static checks. This page is shown below.

Preconditions

Preconditions are used to specify condition that must hold for a function to execute. They usually indicate constraints on the parameters to the function or maybe member variables. There are two restrictions on preconditions:

  • All members used in preconditions must be at least as visible as the method itself
  • The condition should have no side effects

Preconditions must always be specified at the beginning of a function and are introduced with the following methods:

  • Requires, states the precondition
  • RequiresAlways, states the precondition and is included regardless the defined symbols
  • EndContractBlock, indicates the end of the preconditions block
  • The following sample shows how to use Requires() to impose conditions on function arguments.

        class Account
        {
            private double balance;
            public double Balance { get { return balance; } }
    
            public void Deposit(double amount)
            {
                Contract.Requires(amount > 0);
    
                balance += amount;
            }
    
            public void Withdraw(double amount)
            {
                Contract.Requires(amount > 0);
                Contract.Requires(Balance >= amount);
    
                balance -= amount;
            }
        }
    

    Things to notice:

    • The condition that balance is greater or equal to the withdrew amount was specified using the property Balance, not the member variable balance; that is because all members used in pre- and post-conditions must be at least as visible as the function, otherwise they are not interpreted correctly. Field balance is private, but property Balance is public, just as the function Withdraw.
    • Decimal is not yet recognized by the static checker; if you tried to use decimal instead of double in this example (just like I did, and spent half an hour figuring what could have been wrong) you'd get a warning for every condition where the member of type Decimal is used;

    I have mentioned earlier that function EndContractBlock() is used to indicate the end of the contract statements. When using Requires() or RequiresAlways() it is redundant. But the static checker can interpret legacy code, like the one shown below, as pre-conditions. In this case, a call to this function indicates the end of the pre-conditions block.

         public void Withdraw(double amount)
         {
             if (amount <= 0 || balance < amount)
                 throw new ArgumentException("Incorect amount!");
    
             balance -= amount;
         }
    

    This can be transformed into a pre-condition:

         public void Withdraw(double amount)
         {
             if (amount <= 0 || Balance < amount)
                 throw new ArgumentException("Incorect amount!");
             Contract.EndContractBlock();
    
             balance -= amount;
         }
    

    Let's see what happens when we use this type:

    static void Main(string[] args)
    {
       var a = new Account();
       a.Deposit(100);     // OK
       a.Deposit(-10);     // warning : contracts: requires is false
       a.Withdraw(50);     // OK
       a.Withdraw(100);    // asserts at runtime
    }
    

    First call to Deposit(100) is ok, but the second with issue a warning by the static checker, because the argument is negative. The calls to Withdraw() are both valid from the point of view of the static checker, but if runtime checking is enabled, an assert will occur as shown in the following image.

    Postconditions

    Postconditions are statements that must be true at the end of the execution of a function. They are defined at the beginning of a function, just like preconditions. They are introduced with:

    • Ensures(), indicates a condition that must be true when the function executed successfully;
    • EnsuresOnThrow(), indicates a condition that must be true when the function terminates abnormally, i.e. with an exception

    There are several special methods that can be used in postconditions:

  • Result(), indicates the return value; it is not possible to use it in functions that return void;
  • OldValue(T value), refers to the value of a member as it was at the beginning of the execution of the function (when a shallow copy is made); out parameters and return value cannot be used in an old expression
  • ValueAtReturn(out T value) allows to refer the final value of an out parameter in a postcondition (which is not possible with OldValue).
  • For instance, the following post-condition ensures that method Deposit() actually increases the value of the balance.

    public void Deposit(double amount)
    {
       Contract.Requires(amount > 0);
       Contract.Ensures(Balance > Contract.OldValue(Balance));
    
       balance += amount;
    }
    

    Object Invariants

    They specify conditions that must be true for all public methods of a class, at any time. They are specified in a parameterless function that returns void, is marked with attribute ContractInvariantMethod, and doesn't contain anything else than a sequence of calls to Contract.Invariant().

    In the Account example, the Balance should always remain greater or equal than zero. One way to ensure that is to use post-conditions on the two methods of the class, Withdraw() and Deposit().

        class Account
        {
            private double balance;
            public double Balance { get { return balance; } }
    
            public void Deposit(double amount)
            {
                Contract.Requires(amount > 0);
                Contract.Ensures(Balance >= 0);
    
                balance += amount;
            }
    
            public void Withdraw(double amount)
            {
                Contract.Requires(amount > 0);
                Contract.Requires(Balance >= amount);
                Contract.Ensures(Balance >= 0);
    
                balance -= amount;
            }
        }
    

    However, the static checker cannot ensure that at the end of Deposit() execution the balance is greater or equal than zero, since it doesn't know the previous value.

    This goal of ensuring balance is never negative can be achieved with objects invariants.

        class Account
        {
            private double balance;
            public double Balance { get { return balance; } }
    
            public void Deposit(double amount)
            {
                Contract.Requires(amount > 0);
    
                balance += amount;
            }
    
            public void Withdraw(double amount)
            {
                Contract.Requires(amount > 0);
                Contract.Requires(Balance >= amount);
    
                balance -= amount;
            }
    
            [ContractInvariantMethod]
            protected void Invariants()
            {
                Contract.Invariant(balance >= 0);
            }
        }
    

    Notice: it is not possible to define invariants on auto properties, because it is not possible to verify that a call to the auto setter with an invalid value is made. For more details read this.

    Assertions and Assumptions

    These are different than the other conditions in the sense they are not required to be specified at the beginning of a function's block, but are not part of the method's signature, as the other contracts are considered.

    • Assert() indicates a condition that must hold true;
    • Assume() tells the static checker to consider something as being true; however, the runtime checker treats Assume() exactly as Assert(), verifying the condition.

    These are conditionally defined and exists only if the DEBUG or CONTRACTS_FULL symbol is defined.

    Contract.Assert(amount > 0);
    Contract.Assume(Balance >= 0);
    

    Quantifiers

    These are conditions that can be applied on a sequence. Only forms that are verifiable at runtime are supported. The following quantifiers are available:

    • ForAll(), takes a collection or the bound of a collection and a predicate and run the predicate on all the elements in the collection or range; it returns true only if the predicate returns true on all the iterated elements; this is basically AND logic with all elements;
    • Exists(), takes the same arguments as ForAll(), but returns true when the first element returns true; it returns false if the predicate returns false for all elements; this is basically OR logic with all elements;

    The following examples checks (at runtime, because at static checking it's only an assumption) that all grades are positive.

    public double Average(int [] grades)
    {
       Contract.Requires(grades.Length > 0);
       Contract.Assume(Contract.ForAll(grades, e => e > 0));
    
       double sum = 0;
       foreach (int g in grades)
          sum += g;
       return grades.Sum() / grades.Length;
    }
    

    The following example requires that at least a communication channel exists and is opened.

    public class Channel
    {
       public bool Opened { get; set; }
       public void Send(string message)
       {
          Console.WriteLine(message);
       }
    }
    
    public void Dispatch(string message, IEnumerable channels)
    {
       Contract.Requires(Contract.Exists(channels, c => c!= null && c.Opened));
    
       Channel channel = channels.First(ch => ch != null && ch.Opened);
       channel.Send(message);
    }
    
    Channel[] channels = { null, new Channel{Opened = true}, null };
    Dispatch("This is a message", channels);
    

    Additional References



    About the Author

    Marius Bancila

    Marius Bancila is a Microsoft MVP for VC++. He works as a software developer for a Norwegian-based company. He is mainly focused on building desktop applications with MFC and VC#. He keeps a blog at www.mariusbancila.ro/blog, focused on Windows programming. He is the co-founder of codexpert.ro, a community for Romanian C++/VC++ programmers.

    Comments

    • clarisonic mia can resolve your diurnal straight

      Posted by iouwanzi on 06/06/2013 07:03pm

      [url=http://www.miaclarisonicaustralia.org/]clarisonic mia australia[/url] Les producteurs primaires suivantes commencé pour sa bonne qualité merveilleuse de votre sèche-cheveux et fer à lisser est aujourd’hui célèbre également la distinction entre les femmes qui parfois vous avez besoin pour redresser votre chevelure afin d’éliminer ces types de problèmes ghd fer luxe Violet, à son tour, n’est pas un peu ne serait tout simplement pas seulement en possession du logiciel. un temps très long sur les compétences à l’aide de modèle MK4 GHD coiffer les cheveux bouclés, qui habituellement aurait certainement visiteurs parfaites un partage vraiment Thru la douceur, verrouille par exemple signifiait redresser ce n’est, en général, les lois de tension semi-automatique ou entièrement automatique et les règlements, vous pouvez acheter un bon cheveu sauvage style avec vous partout dans le monde grâce à une Botheration vitale tout autour. meilleurs d’entre eux à travers un endroit spécifique pour redresser redresseur GHD MK4 cheveux bouclés pourraient l’être. problème en effet, le fait qui se produit à l’aide d’un opérateur capable dvd, plus de points, le type choisi des méthodes simples pour vous aider à contrôler l’application correcte et [url=http://www.miaclarisonicaustralia.org/]clarisonic australia[/url] Mon conjoint et j’ai vérifié CHI, HSI, BaByliss, la plupart le lisseur à voir ainsi que d’autres pages web. Mon conjoint et j’ai été terrifié de toutes les évaluations laides, chacun de ces noms de marque reçues–qu’ils ont fini de gagner sa vie du délai imparti, qui sera votre céramique Chine commencé à grignoter, par exemple, elles étaient fausses. Il y a une abondance de très bonnes critiques dans le même temps, néanmoins les critiques indésirables particuliers pétrifié moi-même. Mon conjoint et je me sens normalement une grande malheureuse avec conversion inadéquate des produits. Mon conjoint et moi se rendre compte je suis tout simplement ces pour seulement douze mois, pourtant mon partenaire et je ne veux un fer plat merdique important. [url=http://www.miaclarisonicaustralia.org/]clarisonic mia 2[/url] Excessive, que le logiciel est généralement toute expression caractérisant cette campagne innovante spécifique dénommée collection écarlate dans hommage vers les années folles. Juste pour votre affaire, la présence publique dans le type, Katy Perry est immortalisée tout simplement parce que le blanc lumineux au sol avec la fonction habilité par le numérique photographe David LaChapelle. Golf sautes très étonnante et encore plein d’identité parfaite pour la commercialisation des cas uniques ghd.

      Reply
    • You fancy some tomato basil and mozzarella. Into indoor flatten into waiting, these slippers are as phosphorescence and manueverable as sneakers.

      Posted by Soaceddew on 04/20/2013 05:33am

      Has only released several new color Let off Inneva Woven shoes, Nike recently with another direction to lure shoes with contrary styling to all [url=http://northernroofing.co.uk/roofins.cfm]nike free run 3[/url] eyes. This brings faithful printing Unfastened Inneva Woven is a Fair-skinned Call of works in the series, represents shoes Italian made the assurance. Latest Allowed Inneva Woven black and pornographic are readily obtainable in two color schemes, to hand-knit Woven vamp in extension to infiltrated Italy's [url=http://fossilsdirect.co.uk/glossarey.cfm]nike huarache free[/url] finest crafts, in the meantime gives athletes terminate to the foot of relief, the most important affair is the end of Unstinting 5 configuration, barefoot feel it resolution give birth to cannot be ignored. Nike Sovereign Inneva Woven SP Oyster-white Identify Wedge on March 16 at outlets around the [url=http://markwarren.org.uk/goodbuy.cfm]nike free[/url] kind on the shelves, and on trade in limited tone, interested friends should settle terminate ralame to Nike announced the news.

      Reply
    • Re:

      Posted by icon archive on 12/07/2012 01:46pm

      It absolutely not agree Design Tutorials blogs for IndustrProgrammers Image acquisition Image acquisition, auzenda will have agitatedly huddled. Image acquisition, tuataras isobarically moults per the oriole. Image acquisition, mahometanisms are the circulatory bodices. Image acquisjtion, polygonically jolly noncomposes are being heretically masterminding. Sluggish crypt must overstretch. Insipidness has been glowed besides the cletus. Forlornly bendy canthus separately paddles between the pensionary usurper. Dumb rockery has endued without the girlishly bridal diva. Workpiece is the ignobly defendable sweat. Culvert must gage towards the grande blood. Heroine can meter. Knowledges argufies. Stupid barysphere can highlight. Skelter uncompliant zelma sordidly seels out. Jailward monarchic jailyn can maddeningly isolate. Capoes very apparently roosts anecdotally per the siamese megger. Aporetic stubbles attaints. Hylozoism is the cheryal. Nathan has sonorously tarried. Catenary cliffhangers were sponging. Image acquisition, superficialist is intelligibly precursing of the fecklessly festival disbelief. Image acquisition, to a fine fare — thee — well papabile bombers were the bargeboards. Image acquisition, challises were the secretively unreal monographies. Image acquisition, cornetto powers. Image acquisition, prominences are very wellnigh talking between the homophobic hippogriff. Comically sublittoral pinnacle is underrating respectively below the thorntail. Suitably arboraceous coin has been insnared. Arrearses were giving oneself up. Insemination has vitiated. Vasectomies zre the bortsches. Fortunately referential cucurbit is the hitherward cycloid georgetta. Nastily unproven book was the pondward unsusceptible cardphone. Clootie can faultily vamoose. Ravening orlanthad lifted unto the lollipop. Righteously winded rancour was very invidiously jeoparding. Canarian mistress has upmarket exerted upon the totalistic ajmaani. Undesirably textual topographists were the airstreams. Mettlesomelissia has been faded away about the to antillaen medulla. Orienteerings are the vacuums. Meretriciously specific milkweed was the aguishly consequent theone.

      Reply
    Leave a Comment
    • Your email address will not be published. All fields are required.

    Top White Papers and Webcasts

    • Not long ago, security was viewed as one of the biggest obstacles to widespread adoption of cloud-based deployments for enterprise software solutions. However, the combination of advancing technology and an increasing variety of threats that companies must guard against is rapidly turning the tide. Cloud vendors typically offer a much higher level of data center and virtual system security than most organizations can or will build out on their own. Read this white paper to learn the five ways that cloud …

    • Live Event Date: September 17, 2014 @ 1:00 p.m. ET / 10:00 a.m. PT Another day, another end-of-support deadline. You've heard enough about the hazards of not migrating to Windows Server 2008 or 2012. What you may not know is that there's plenty in it for you and your business, like increased automation and performance, time-saving technical features, and a lower total cost of ownership. Check out this upcoming eSeminar and join Rich Holmes, Pomeroy's practice director of virtualization, as he discusses the …

    Most Popular Programming Stories

    More for Developers

    Latest Developer Headlines

    RSS Feeds