Like the Contract.ForAll, the Contract.Exists method comes in two flavors, one that takes two integers as lower and upper bound and a Predicate<int>, and a generic one that takes an IEnumerable<T> and a Predicate<T> as input. And where the Contract.ForAll method checks that any entry that is passed to the given Predicate returns true, the Contract.Exists method will return true if at least one of the entries returns true on the Predicate.

Let’s give a simple example. With the ForAll method  gave an example that would test a list for having the ten prime numbers greater than a given value x. It actually omitted an additional check which is the following:

      Contract.Requires(Contract.ForAll(0, primeList.Count - 1, p => primeList[p] < primeList[p + 1]));

This checks that for all items in the list, the next value is actually greater than the preceding one. In order to do something similar with the Contract.Exists method, lets write a method that requires at least one of the given numbers is prime:

    public List<int> FindAtLeastOnePrimeFollowingX(int x, List<int> numberList)
    {
      Contract.Requires(x > 0);
      Contract.Requires(numberList != null);
      Contract.Requires(numberList.Count > 5);
      Contract.Requires(Contract.ForAll(0, numberList.Count, p => numberList[p] > x));
      Contract.Requires(Contract.ForAll(0, numberList.Count - 1, p => numberList[p] < numberList[p + 1]));
      Contract.Requires(Contract.Exists(0, numberList.Count, p => numberList[p].IsPrime()));
 
      return (from p in numberList
              where p.IsPrime()
              select p).ToList();
    }

This is just an example showing the working of the Code Contracts methods. I have no intention to bring this as a real world example. I probably will come up which such an example in a later stage. The last precondition in the example checks the requirement that there must be at least one prime number in the list passed as the second parameter. I was going to insert a post condition in here as well, which would ensure that in the result I would also have at least one prime number, but the ensures fails with the warning:

CodeContracts: ensures unproven: Contract.Exists(Contract.Result<List<int>>(), p => p.IsPrime())

Even though the predicate on the IsPrime is in the LINQ statement, the static checker is currently not able to project this also onto the post condition that I defined. Maybe this will get better in the near future.

Next post in the series will be about the Contract.Assume method, which can be used to indicate to the static checker that even though static analysis on its own isn’t able to prove certain facts, the fact is still true and should be treated as proven.

That’s it for now
Meile