Using quantifiers on Code Contracts

Code Contracts also supports are quantifiers (with several limitations, as we’ll see). This means that you can check a predicate against elements in a collection or interval. You can use the ForAll method for running a predicate over several elements maintained on an collection or interval. The Exists method will let you apply a predicate and see if there is at least one item in the  specified collection or interval that validates that predicate.

Consider these two classes:

public class Person {
        public String Name { get; set; }
}
public class PersonSearcher {
        private String _name;
        private IEnumerable<Person> _people;
        public PersonSearcher SearchFor(String name) {
            _name = name;
            return this;
        }
        public PersonSearcher OnPeople(IEnumerable<Person> people) {
            _people = people;
            return this;
        }
        public Person Get() {
            return _people.SingleOrDefault( p => String.CompareOrdinal(p.Name, _name) == 0);
        }
}

There’s a simple Person class and a PersonSearcher class which checks if a specific person in on a collection of Persons. Suppose that one of the things we’d like to make sure is that all the items on the people collection that are passed as a parameter are non null. This is easily done by using the ForAll method:

public PersonSearcher OnPeople(IEnumerable<Person> people) {
    CodeContract.Requires(
                         CodeContract.ForAll(people, p => p != null));
    _people = people;
    return this;
}

And now you do get verification on all the instances of people passed as an argument. For instance, if you try to run this code, you’ll get a Debug.Assert at runtime:~

var people = new[]
                             {
                                 null,
                                 new Person {Name = "Luis"},
                                 new Person {Name = "John"},
                                 new Person {Name = "Charles"}
                             };
new PersonSearcher().SearchFor("Luis").OnPeople(people);

If the method received an array, you could also use the other overload method:

public PersonSearcher OnPeople(Person[] people) {
  CodeContract.Requires(
   CodeContract.ForAll(0, people.Length, pos => people[pos] != null));
CodeContract.Ensures(_people != null);
_people = people;
return this;
}

The Exists method is really similar to the ForAll method, so I won’t be writing any example to show its usage. On the next post, we’ll start looking at runtime behavior. Keep tuned!