log in

.NET 4.0: Code Contracts and Pex

Luke Breuer
2009-02-24 18:52 UTC

PDC 2008 Contract Checking and Automated Test Generation with Pex

The contracts library is now available.

Specific comments can be sent to: codconfb at microsoft dot com

Mike Barnett (worked on Spec#)
Nikolai Tillmann (MS Research)

.NET 4.0 will have a Contract Library which is language-agnostic. This can be downloaded from Microsoft Research.

Say we have:
string s = o.GetDescription(i);
What are allowable values for i? Can any exceptions be thrown? What is guaranteed about the return value of GetDescription?

The contract library allows this:
string GetDescription(int x)
    Contract.Requires(0 < x);
    Contract.Ensures(Contract.Result<string>() != null);

Located in System.Diagnostics.Contracts (CodeContract in current CTP).
  • contracts document design decisions
    • preconditions, postconditions, invariants
    • facilitate code evolution
  • contracts are executable
    • checked documentation
    • test oracles
  • contracts help static verification
    • early error detection
    • clarify responsibility at API boundaries
  • assertions help, but everyone has their own flavor
    • difficult to tool against
    • note seen as a contract between two parties

The static checker will do things like divide-by-zero checks without any code — it just knows to check these things. It will take possible subclasses into account in the static analysis.
Possible Contracts
  • Requires
    • what must be true at method entry
  • Ensures
    • what must be true at method exit
    • can also specify behavior when an exception is thrown
  • Invariants
    • what must be true for all methods in the class (including subtypes)
  • Assertions, Assumptions, ...
    • see documentation

Any boolean expression can be passed to contracts.

There are two forms of contract "declaration" — one will result in conditional compilation so that the contracts are not included in "Release" builds, and one that will always be included. This might be useful if you want your public API entry points to always have contracts apply.

The contract tooling can generate "reference assemblies" that include all the contracts so that while the release builds do not have contracts, customers can still access contract information.

Can define contracts on interfaces by creating a class that mirrors the interface and has the actual contract code.

Examines IL; runs after compilation.
Pex will analyze examining code, including branches, and generate test cases. It can be downloaded for VS2008 and VS2010. Pex finds edge cases and lists them, along with stack traces (because Pex actually runs the code). Pex can automatically create a test project that includes a test it created. The result is that you can take an existing piece of code, use Pex to find an edge case that produces an exception or violates a contract, and then debug to the failure point to explore what might have went wrong.

Test suites generated by Pex can also be used to characterize code. Before changing code, generate a test suite. After changing the code, see if any tests have started failing.

Pex can also be used just to understand code. It can generate test cases that will execute any line of code desired (assuming it's good at getting high code coverage). In examining code, one can add "internal" assertions (which the end-user might not care about) in attempting to understand the code, then run Pex to see if those assertions actually hold.

Taking NHibernate's TypeNameParser, Pex was able to get 100% code coverage.

Pex does not guess:
  • it does not generate random inputs
  • it does not enumerate possible values
  • it does not make you write test input generators

Instead, Pex analyzes .NET code:
  • partitions inputs into equivalence classes
  • one equivalence class per branching behavior
  • test inputs computed by Z3, the world class constraint solver for program analysis from Microsoft Research
  • precise, inter-procedural, path-sensitive analysis

Pex only emits test cases if they increase code coverage.

One can write "parametrized tests" which means declaring a test method with inputs that Pex will populate with intelligent, edge-case-triggering values. This can be particularly useful for TDD.

When changing functionality, Pex will keep around the test cases that aren't affected, might delete some old test cases, and will probably create some new ones.

Pex does not scale well past a few thousand lines of code. It should be used with a "unit testing spirit", which means smaller pieces of code.

Pex comes with a framework so that objects can be specified for interfaces so Pex can pass interfaces into methods and such.

Pex can identify tests that would violate contracts, aren't interesting, and thus can be deleted.