This post in the series on Code.Contracts is all about the Contract.ForAll method. It comes in two flavors, one that iterates in a for-loop way, and a generic form that iterates over an IEnumerable of T in a more foreach kind of way.

In the example I have used so far, I included at one point the check with Contract.ForAll<char> to ensure all the characters in the result must be equal to the first character of the input string. Unfortunately the static checker of Code Contracts is unable to ensure the correctness of this for all test. It probably has got to do something with the fact that the current System.String implementation does not include the contract checks on the constructor we’re using. Hence the checker presents you with a warning like this:

CodeContracts: ensures unproven: Contract.ForAll(0, count, p => Contract.Result<string>()[p].Equals(input[0]))

I’ve tried a few things to work around this warning, but haven’t had any luck so far. So if anyone has a brilliant idea how to get rid of it, be my guest.

So I created a different example to explain the Contract.ForAll method, which will be proven nicely by the static checker. Here goes:

    public bool FirstTenPrimesFollowingX(int x, List<int> primeList)
    {
      Contract.Requires(x > 0);
      Contract.Requires(primeList != null);
      Contract.Requires(primeList.Count == 10);
      Contract.Requires(Contract.ForAll(0, primeList.Count, p => primeList[p] > x));
      Contract.Requires(Contract.ForAll<int>(primeList, p => p.IsPrime()));
 
      return (from p in primeList
              where !p.IsPrime()
              select p).Count() == 0;
    }

This example tests whether the list of primes in the second parameter will only contain the next ten primes greater than the value in the x input parameter. There is a number of preconditions present, all of them checking a bit of the contract. The first ensures the value of x is greater than 0, the second makes sure the list of primes is not null, the third ensures the count of the given list is 10. The fourth is a call to Contract.ForAll, this is the first flavor mentioned above. It iterates from 0 to the count of the primeList, and ensures each value is greater than x. The fifth and last check is using the second flavor of Contract.ForAll, which is the generic form. In this particular case, the type of int could have been inferred from the usage, but I’ve chosen to put it here explicitly to make it clear we’re calling the generic form of Contract.ForAll. It validates that each entry in the list is indeed prime.

Let me note that there is no real world purpose to the example’s method body. It simply confirms that there is no non-prime value in the list, which is already ensured by the method’s contract. As may have become clear from the example, the Contract.ForAll is not restricted to Contract.Ensures calls. It’s not even restricted to any Contract calls. However, be aware of how and when to use this.

The next post I will take the Contract.OldValue<T>() method as the subject. This is a method that is restricted to usage in post conditions. And there is still some ground to cover on the end of the post conditions, as there is also the Contract.ValueAtReturn<T>() method and the other post condition Contract.EnsuresOnThrow<TException> method as well.

That’s it for now
Meile

The previous post was about post conditions, and more specific the Contract.Ensures method. In the example I used another method on the Contract class, Contract.Result<T> to get the eventual result of the method. The Contract.Result<T> has been backed in to give the programmer a convenient way to get the result of the method beforehand.

The T defines the type of the return value, and logically it must match the return type of the enclosing method body. The return value of the Contract.Result<T>() method call is the actual return value of the enclosing method. The method can only be used in Contract.Ensures() method calls. So this is not some convenient way to get the return value beforehand at any place in your method body.

To refresh the memories a bit, here’s the example again:

    public string RepeatFirstCharacter(string input, int count)
    {
      Contract.Requires<ArgumentNullException>(input != null);
      Contract.Requires<ArgumentException>(input.Length >= 0, "The input should have at least one character.");
      Contract.Requires<ArgumentOutOfRangeException>(count > 0);
      Contract.Requires((0 + 1) <= input.Length);
      Contract.Ensures(Contract.Result<string>().Length == count);
 
      return new string(input.ToCharArray(0, 1)[0], count);
    }

The Contract.Ensures call now verifies that the return value of the enclosing method has actually got a length that is equal to the count input parameter’s value. I’ve also added another precondition, since the static code checker of Code Contracts proposed another precondition, to ensure the result can be correctly computed. It’s the following line:

      Contract.Requires((0 + 1) <= input.Length);

This ensures the result can use the ToCharArray(0, 1) code without a possible exception being thrown at you at runtime. In my last post I also referred to the Contract.ForAll<T> method. This will actually be the subject of the next post in this series.

That’s it for now
Meile