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