Pex and Contracts: Better Together

Pex is an automatic unit tests generator that seamlessly integrates with Visual Studio IDE. Contracts is an implementation of a concept (or technique) called Design by Contract (DBC). In this post I will show how to use Pex and Contracts together to improve code quality.

Some time ago I was working on an application where I needed to dynamically load only the types implementing certain interface from certain assemblies. I will not go into details on how to solve the problem of dynamic loading types, but will do on how to use Pex and Contracts to generate test cases with high code coverage, using the class I created to accomplish the task as example (by the way, I might have used the Managed Extensibility Framework to load the types, but in such case I had not been able to write this post).

I implemented a Helper class that can find types implementing a given interface, looking for all types in an assembly. The class can also ensure that it is possible to create instances of those types, looking for the constructors among the instance methods. Then the class can invoke the constructor to create new instances of those types.

Here is the code of the Helper class I will be using in this post:

public class Helper
{
    public static IEnumerable<Type> LoadTypesFrom(
        string assemblyName, string interfaceName)
    {
        List<Type> result = new List<Type>();
        Assembly assembly = Assembly.LoadFrom(assemblyName);
        Type[] typesInAssembly = assembly.GetExportedTypes();
        foreach (Type type in typesInAssembly)
        {
            if (type.GetInterface(interfaceName) != null)
            {
                result.Add(type);
            }
        }
        return result;
    }

    public static IEnumerable<FileInfo> GetDllsIn(string path)
    {
        List<FileInfo> result = new List<FileInfo>();
        DirectoryInfo directoryInfo = new DirectoryInfo(path);
        foreach (FileInfo item in directoryInfo.GetFiles("*.dll"))
        {
            result.Add(item);
        }
        return result;
    }

    public static object CreateInstance(Type type)
    {
        ConstructorInfo ctor = type.GetConstructor(
            BindingFlags.Instance | BindingFlags.Public, null,
            CallingConventions.HasThis, Type.EmptyTypes, null);
        return ctor.Invoke(Type.EmptyTypes);
    }
}

The method LoadTypesFrom receives the name of an assembly, including the path, and the name of an interface, and returns a list of all types in the given assembly that implement the given interface.

The list is returned as IEnumerable<type> and not as IList<type> or ICollection<type> to prevent Helper class clients to accidentally modify the list by removing or adding other types that could possibly not implement the given interface.

The method works by loading the assembly from the given path with a call to Assembly.LoadFrom. Then it gets all the types in the assembly by using Assembly.GetExportedTypes. Finally, it iterates among these types, and determines whether or not to each type implements the interface, using Type.GetInterface. The types that implement the interface are added to the result.

The method GetDllsIn receives a full path to a folder and returns a list of all files with .DLL extension in that folder. The list is also returned as an IEnumerable<FileInfo> for the same reasons mentioned for the previous method.

The method simply uses DirectoryInfo.GetFiles to get the list of files.

The CreateInstance method receives a type as a parameter and returns an instance of that type.

The method first looks for a constructor without parameters using Type.GetConstructor and then it creates an instance by calling the constructor using ConstructorInfo.Invoke.

We will create unit tests in Visual Studio (previously we need to install Pex and Contracts; details on how to download and install both appear at the end of this post).

Here comes the magic. We right click on LoadTypesFrom method declaration, and then we click on the Run Pex menu item to invoke Pex.

Pex uses parameterized unit tests (PUT). A PUT is simply a method that takes certain parameters, invokes the code being tested, and tests if certain assertions are satisfied or not. For a PUT written in one of the .NET languages, Pex automatically produces a small test suite with high code coverage. Also, when a generated test fails, Pex can often suggest a solution. Pex runs and analyzes the code under testing, learning about the program’s behavior by monitoring its implementation, and generates new test cases with different behavior.

When Pex runs for the first time, it founds an ArgumentNullException exception and shows what it has found:

We started very well. When programming Helper.LoadTypesFrom I did not realize that if assemblyName is null the method will not work; I should have controlled it. Fortunately Pex tried to run LoadTypesFrom(null) and found the problem.

Typically we solve this by adding

if (assemblyName == null) throw new ArgumentNullException("assemblyName");

at the beginning of the method. It is a good programming practice to check that arguments are not null if when they are null the method does not work. But two things that are not properly solved even with this good practice:

1. We cannot explicitly declare the prerequisite that the method requires a non-null argument. We can state that in the documentation, and we can also state in the documentation that an ArgumentNullException exception will be thrown if the argument is null (assuming other developers will read the documentation). But we cannot prevent a developer (not even ourselves, some timer after writing the code) to forget that the argument cannot be null.
2. We cannot get the program to stop compiling or at least giving us a warning if (by accident) we wrote LoadTypeFrom(null). Not only do we have to be able to state the prerequisites of the method, but also the tools must be able to interpret and validate these prerequisites.

Here is where Contracts comes in.

The roots of this concept can be found in the fundamentals of software correctness proposed by C. A. R. Hoare and others a long, long time ago, who pursue ways to write correct programs and knowing they were correct! More recently Bertrand Meyer popularized the concept with the Eiffel programming language.

The key behind design by contract is that in order to determine whether a program is correct or not, we must first have a specification of what the program should do. Once we get that specification, deciding whether the program is correct or not is straightforward: if the program does what is specified, then it is correct; on the contrary, it is not.

I do not want to bore you with details about design by contract. It is enough for now to say that, applied to the object-oriented programming paradigm, a program specification is given by:

1. Preconditions. These are predicates (assertions which may be true or false) in the context of a method that must be satisfied in order to invoke the method. The responsibility of the predicate being true is on the class who invokes the method: either it makes the predicate fulfilled, or it cannot invoke the method. On the contrary, it is a benefit for the developer of the method knowing that the predicate is true when the method starts, and he can build from that.
2. Postcondition. They are predicates in the context of a method expected to be true when the method returns. The responsibility of making the predicate evaluate true, is now on the developer of the method; he mandatory needs to code the method in such a way to satisfy the postcondition at the end of the method. On the contrary, postconditions are a benefit to the class invoking the method: it knows that when the method returns, the predicate is true, and can continue from that fact.
3. Invariant. They are predicates in the context of a class that are true throughout the entire life of each instance. Invariants are like preconditions and postcondition added at the beginning and the end of each instance method (and at the end of the constructors).

The Microsoft Research’s Contracts project of is not the first Microsoft attempt to add design by contract to C#; probably you have heard about the Spec# project.

Contracts implementation is brilliant once you know all the restrictions that its design team had to overcome:

1. They could not touch the CLR.
2. They could not change the syntax of the language.
3. They could not change compilers.
4. They should make Contracts available in as many languages as possible.

The reasons for these restrictions come, in first place, from the amount of languages that the .NET Framework supports; do not forget there are other languages in addition to C# or Visual Basic; and secondly, playing with the CLR can be a source of instability of the .NET Framework itself.

The solution was:

1. Create a set of classes to implement preconditions, postcondition and invariant. The same classes can be used from any language.
2. Integration with Visual Studio to control assertions at design time. Violations of the assertions should appear in the list of errors when compiling.
3. Inject code at compile time to implement the behavior associated with the assertions. For example, the postcondition can be placed anywhere in the method, but in the generated code always appear at the end.

The main class you use to implement design by contract is Contract class. In Visual Studio 2008 and. NET Framework 3.5, in order to use this class you need to manually add the assembly Microsoft.Contracts.dll, located in %ProgramFiles%\Microsoft\Contracts\PublicAssemblies\v3.5, to the list of project references. In Visual Studio 2010 and. NET Framework 4.0, the assembly is already in the list of references by default. In any case, you should include a reference to the namespace System.Diagnostics.Contracts with a using clause in the source files where you plan to use the Contract class. Finally, you must enable contracts checking at design time and at runtime, by using the Code Contracts tab in project’s properties:

This entire introduction is needed to understand that the real way to specify that an argument cannot be null is:

public static IEnumerable<Type> LoadTypesFrom(
    string assemblyName, string interfaceName)
{
    Contract.Requires(assemblyName != null);
    Contract.Requires(interfaceName != null);
    …

The preconditions are declared with Contract.Requires. The argument of Requires is an assertion that may be true or false. If in some place in the code there were a call like Helper.LoadTypesFrom (null, null), the compiler will show it:

The message Contracts: Requires is false corresponds to the line

Helper.LoadTypesFrom(null, null);

while the message + location related to previous warning corresponds to the line

Contract.Requires(assemblyName != null);

How does Contracts affects test cases generation with Pex?

When we run Pex again in the method LoadTypesFrom, more test cases and more clues appear for further completing the specification of the method:

The last error message suggests that we can add two new preconditions to LoadTypesFrom:

Contract.Requires(assemblyName.Length > 0);
Contract.Requires(interfaceName.Length > 0);

The last error message suggests again a precondition, but the assertion clause is more complex than previous ones, because somehow we must specify that each and every one of the characters in the string is valid. This type of predicate requires what is called a universal quantifier: Contracts.ForAll. The ForAll method is overloaded; the way they are going to use it requires an IEnumerable and Predicate:

Contract.Requires(Contract.ForAll<Char>(
    Path.GetInvalidPathChars(),
    (Char c) => !assemblyName.Contains(c.ToString())));

The second argument is a lambda expression that is evaluated for each element of the first argument.

When we run Pex again, we see how the actual test case exercises the precondition added, and again the last error message gives us clues about a new precondition:

The new precondition is:

Contract.Requires(assemblyName.Trim() == assemblyName);
Contract.Requires(interfaceName.Trim() == interfaceName);

Pex generates even more test cases and, as before, there is a new error message:

When we add the precondition [1]

Contract.Requires(File.Exists(assemblyName));

Pex generates eleven test cases without further messages.

We are done? Not yet. Remember that the preconditions are obligations for those who invoke the method LoadTypesFrom. But, what are the obligations of LoadTypesFrom? Or put in another way, where it is specified what LoadTypesFrom does?

It is time to add postconditions. The postconditions are added with Contract.Ensures:

Contract.Ensures(Contract.Result<IEnumerable<Type>>() != null);
Contract.Ensures(Contract.ForAll<Type>(
    Contract.Result<IEnumerable<Type>>(),
    (Type item) => item.GetInterface(typeName) != null));

The first postcondition specifies that the result is never null. This means that when types are not found in the given assembly, the method returns an empty list but not null [2] .

The second postcondition also includes a universal quantifier. In prose, the postcondition specifies that all types returned as a result, implement the interface passed as argument, which is exactly what I tell you when I described the method above!

That is just the beauty of design by contract: it is possible to describe what a program does (a method in this case) unequivocally, unambiguously and automatically verifiable way. In addition, as assertions always accompany the code, they are easy to find and easy to keep updated.

But let us go back to Pex. To save generated test cases, we select them, then we right-click the on the selection, and then we choose Save…:

Pex shows us what it will do next, step by step:

After Pex makes the changes announced, the solution will have a new test project that we can compile and run like any other:

Before running the test cases generated by Pex, let us talk a little bit about code coverage.

One of the objectives of using Pex is to generate the smallest number of test cases that ensure the largest possible code coverage. The code coverage of test cases, or simply coverage, is the number of lines of code executed during test runs. If coverage is low, there are potentially some lines of code not reached during the tests that can contain bugs. We cannot say there are bugs, but we can say that if there are errors in the lines not executed, we will not find them.

On the contrary, high coverage is no guarantee of better test cases or absence of errors, but if you let me choose, I prefer the largest possible coverage.

To measure the coverage you need first to change test run configuration. We click on Test, then click Edit Test Run Configurations, and then click on the desired setting, which by default is Local Test Run:

Once there we select Code Coverage from the list and mark the assembly we want to measure coverage from the list Select artifacts to instrument.

To run the test cases we click on Test, then on Run, and then we choose All Tests in Solution. At the end we get the result:

We do not know yet if LoadTypeFrom method works or not. To find it out, we can generate a test case to find a class that implements an interface that we know for sure that is in certain assembly. We can add an interface and a class that implements that interface in the same place where the test cases generated by Pex are, like these ones:

public interface Foo { }

public class Boo : Foo { }

Then we add a method like this:

[TestMethod]
public void TestLoadTypesFrom()
{
    IEnumerable<Type> result = Helper.LoadTypesFrom(
        Assembly.GetExecutingAssembly().Location, "Foo");
    bool booExists = false;
    foreach (Type type in result)
    {
        if (type.Equals(typeof(Boo)))
        {
            booExists = true;
        }
    }
    PexAssert.IsTrue(booExists);
}

As the interface Foo and the class Boo are implemented together with the test cases, they are in the same assembly, the assembly running when the test case gets invoked. This assembly is obtained by calling Assembly.GetExecutingAssembly. So we can be sure that the method LoadTypesFrom should return Boo on the list. The foreach loop search for type Boo in the result and PexAssert.IsTrue is used to display the result together with the results of other test cases generated by Pex.

Conclusions

Pex is a project of Microsoft Research, which integrates directly into Visual Studio. It makes a systematic analysis to code, looking for boundary values, exceptions, etc. and so finds interesting entry and exit values of selected methods, which can be used to generate a small test suite with high code coverage.

Contracts is also a Microsoft Research project to apply design by contract in.NET Framework languages.

Each one on its side is very interesting, but when used together, we can create better specifications with Contracts and better test cases with Pex. That is why I say, Pex and Contacts, better together!

References

The homepage of Pex at Microsoft Research is http://research.microsoft.com/en-us/projects/pex/

In MSDN DevLabs is http://msdn.microsoft.com/en-us/devlabs/cc950525.aspx

The homepage of Contracts at Microsoft Research is http://research.microsoft.com/en-us/projects/contracts/

In MSDN DevLabs is http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx

---

[1] Some might say it is not correct to add this precondition it does not indicate a condition on the program but on a file that is external to the program. What we are stating is that the assembly must exist in order to extract types of it.

[2] It is debatable whether the result should be null instead of an empty list. Someone might say you are instantiating an object that is not used then, which negatively impacts performance. I prefer the approach of returning the empty list, because I can always put the result in a foreach loop without fear that it might fail because the null set to go better in this case where the performance impact is minimal.