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

    More by Author

    Get the Free Newsletter!

    Subscribe to Developer Insider for top news, trends & analysis

    Must Read