I recorded a Channel9 video last week with Manuel Fahndrich on the interaction of Code Contracts and Pex. The demo gives a glimpse at the nice interaction between Contracts (design by contracts) and Pex (automated white box).

Code Contracts gives you a great way to specify what your code is supposed to do. These contracts can be leverage for documentation, static checkers but also – tada – by Pex! Contracts can also be turned into runtime checks which Pex will try to explore. Pex will try to cover the post conditions, assertions or in other words, find inputs that violates of your contracts etc… By adding contracts to your code, you give Pex a ‘direction’ to search for (and a test oracle).

Drop me a note if you want more of those movies.