Code Contracts

My first post is about the Microsoft's Code Contracts, because I helped my colleague to apply code contracts on his code yesterday. I've already had some knowledge about the technology, but I've never used it before in a real life project.

So yesterday we found a bug or let's say a missing feature from the code contracts. I post this here because I'm sure somebody else will bump into this problem and probably he or she will find this site and will read about it. The missing feature is handling contracts on decimal values. I won't publish our project code here, but I'll show you the solution and a problem through a prototype class library project that is written by me.

For the example I created an ExampleClass class with four methods.

 /// <summary>
 /// Represents the example class.
 /// </summary>
 public static class ExampleClass
 {
     #region Public Methods

     /// <summary>
     /// Divides the hundred with the specified value.
     /// </summary>
     /// <param name="value">The value.</param>
     /// <returns>100 / value.</returns>
     public static decimal DivideHundred(int value)
     {
         if ( value == 0 )
         {
             throw new InvalidOperationException( "Invalid value. The value cannot be 0." );
         }

         return 100 / value;
     }

     /// <summary>
     /// Divides the hundred with the specified value.
     /// </summary>
     /// <param name="value">The value.</param>
     /// <returns>100 / value.</returns>
     public static decimal DivideHundred( decimal value )
     {
         if ( value == 0 )
         {
             throw new InvalidOperationException( "Invalid value. The value cannot be 0." );
         }

         return 100 / value;
     }

     /// <summary>
     /// Gets the decimal that is not 0.
     /// </summary>
     /// <returns></returns>
     public static decimal GetDecimalThatIsNot0()
     {
         return 1;
     }

     /// <summary>
     /// Gets the integer that is not 0.
     /// </summary>
     /// <returns></returns>
     public static int GetIntegerThatIsNot0()
     {
         return 1;
     }

     #endregion
 }

The DivideHundred method and its overload just use the old way contracts, they throw exceptions on invalid contracts.

Let's change them to use the Microsoft's Code Contracts.

     /// <summary>
     /// Divides the hundred with the specified value.
     /// </summary>
     /// <param name="value">The value.</param>
     /// <returns>100 / value.</returns>
     public static decimal DivideHundred(int value)
     {
         Contract.Requires( value != 0, "value is 0." );

         return 100 / value;
     }

     /// <summary>
     /// Divides the hundred with the specified value.
     /// </summary>
     /// <param name="value">The value.</param>
     /// <returns>100 / value.</returns>
     public static decimal DivideHundred( decimal value )
     {
         Contract.Requires( value != 0, "value is 0." );

         return 100 / value;
     }

Let's implement a "controller" class that is called ControllerClass.

 /// <summary>
 /// Represents a controller class.
 /// </summary>
 public class ControllerClass
 {
     #region Public Methods

     /// <summary>
     /// Tests the conracts.
     /// </summary>
     public void TestConracts()
     {
         var integerValue = ExampleClass.GetIntegerThatIsNot0();
         var result = ExampleClass.DivideHundred( integerValue );
      
         var decimalValue = ExampleClass.GetDecimalThatIsNot0();
         result = ExampleClass.DivideHundred( decimalValue );
     }

     #endregion
 }

In the ControllerClass class I don't check any preconditions, just call the methods from the ExampleClass class.

After the compiling we will get the following warnings:



It's totally okay because the Contract.Requires. Let's change the Get methods. We know that always give 1 to us, so we can ensure the results. Let's do it:

       /// <summary>
       /// Gets the decimal that is not 0.
       /// </summary>
       /// <returns></returns>
       public static decimal GetDecimalThatIsNot0()
       {
           Contract.Ensures( Contract.Result<decimal>() == 1 );

           return 1;
       }

       /// <summary>
       /// Gets the integer that is not 0.
       /// </summary>
       /// <returns></returns>
       public static int GetIntegerThatIsNot0()
       {
           Contract.Ensures( Contract.Result<int>() == 1 );

           return 1;
       }

After the compiling we will get the following warnings:



As we see the integer part of the code was fixed, but the decimal? The decimal part is still wrong. Not even the require is unproven, but the ensure is unproven too. So we have to change the code for the decimal to use the old way, to use the exceptions.

        /// <summary>
        /// Divides the hundred with the specified value.
        /// </summary>
        /// <param name="value">The value.</param>
        /// <returns>100 / value.</returns>
        public static decimal DivideHundred( decimal value )
        {
            if ( value == 0 )
            {
                throw new ArgumentException( "value is 0.", "value" );
            }

            return 100 / value;
        }

        /// <summary>
        /// Gets the decimal that is not 0.
        /// </summary>
        /// <returns></returns>
        public static decimal GetDecimalThatIsNot0()
        {
            return 1;
        }

            var decimalValue = ExampleClass.GetDecimalThatIsNot0();

            if ( decimalValue != 0 )
            {
                result = ExampleClass.DivideHundred( decimalValue );
            }

That's it. We can't use the code contracts on the decimal values yet.