Matthew Podwysocki's Blog

DC ALT.NET 11/25 - Web Testing Frameworks

podwysocki — Mon, 17 Nov 2008 23:22:00 -0600

The November meeting for DC ALT.NET will be on November 25th, 2008 from 7PM-9PM. Check out our site and our mailing list for more information as it becomes available. This month, John Morales will be facilitating a discussion on web testing frameworks which includes Selenium, Watir and WatiN among others. Once again, I'd like to thank Cynergy Systems, Inc for sponsoring this month's event.

The information is as follows:

DateTime:
11/25/2008 - 7PM-9PM

Location:
Cynergy Systems Inc.
1600 K St NW
Suite 300
Washington, DC 20006
Show Map

Functional .NET 4.0 - Tuples and Zip

podwysocki — Sun, 16 Nov 2008 00:05:00 -0600

Previously, when covering some of the additions to the .NET 4.0 Framework such as optional and named parameters, some of the other additions have caught my eye from the perspective of functional programming. Unlike .NET 3.5, this release is not as targeted towards functional programming as it is more towards dynamic programming and COM interoperability. But, there are a few items to note that we can soon take advantage of, including the Tuple type and the Zip operator function among other items.

Looking at Tuples

To define a tuple, it comes from the mathematics field, and is simply an ordered list of values, which are components of that tuple. These components can be of any type, whether it be string, integer, or otherwise. In order to refer to these components, we retrieve references to them by absolute position in that sequence.

In F#, the tuple is a fully supported data type and perhaps one of the most useful. To define a tuple is to define a number of expressions grouped together with comma separation to form a new expression such as the following:

#light  

// val blogger : string * string 
  
let blogger1 = "Matthew", "Podwysocki" 
  
let blogger2 = "Jeremy", "Miller" 
  
let blogger3 = "David", "Laribee" 
  
// val bloggers :  
  
// (string * string) * (string * string) * (string * string)  
  
let bloggers = blogger1, blogger2, blogger3

From there, tuples can be decomposed into their components in either of two ways. For pair tuples, a tuple with exactly two components, can be deconstructed using the fst and snd functions such as the following:

#light 
  
let pageHitCount = "http://www.codebetter.com/", 25500 
  
let page = fst pageHitCount 
  
let hitCount = snd pageHitCount

However, it is more common to use a pattern expression to retrieve values from a tuple, such as the following code:

#light 
  
let request =  
  "http://codebetter",  
  new DateTime(2008, 11, 15), 
  
  "Firefox/3.0.4 (.NET CLR 3.5.30729)"

  
let host, date, userAgent = request

What we're able to do is break down the given request into three pieces, the host, date and user-agent. This makes pattern matching against tuples really powerful such as the following:

#light 
  
// val permit_request : string * string * int -> bool 
  
let permit_request = function 
  
  | "http", "google.com", 80 -> true 
  
  | _, "microsoft.com", _ -> true 
  
  | "ftp", _, 21 -> true 
  
  | _ -> false

Just as well, we could even use them in active patterns so that we could pattern match against parts of a FileVersionInfo in order to determine which action to take such as the following.

#light 
  
open System.Diagnostics 
  
let (|FileVersionSections|) (f:FileVersionInfo) =  
  (f.FileName,f.ProductName,f.ProductVersion) 
  
let parse_files = function 
  
  | FileVersionSections(fn, "Parallel Extensions for the .NET Framework", _)  
      -> printfn "Parallel Extensions file %s" fn 
  
  | FileVersionSections(fn, "Microsoft Office Communicator 2007", _)  
      -> printfn "Communicator file %s" fn 
  
  | _ -> printfn "Unknown file"

You're saying, great, but what has this to do with .NET 4.0?

Tuples in .NET 4.0

Earlier this month, Justin Van Patten, on the BCL Team Blog announced some the base class library changes coming to .NET 4.0. Among them was Tuples in which was stated:

We are providing common tuple types in the BCL to facilitate language interoperability and to reduce duplication in the framework. A tuple is a simple generic data structure that holds an ordered set of items of heterogeneous types. Tuples are supported natively in languages such as F# and IronPython, but are also easy to use from any .NET language such as C# and VB.

What does that mean exactly? Does this mean we'll get some form of syntactic sugar around them as well? If we could decompose them in such a fashion as we do in F#, and to initialize them in an easy fashion without a lot of pomp and circumstance. Gazing from the intent in the .NET libraries, something like this might be an option:

var t1 = Tuple.Create(1, 'a');  
var i1 = t1.Item1;  
var i2 = t1.Item2;

But, unless there were a nicer way to tease apart the data, it just becomes a simple holder of data, instead of something that we could decompose easily into patterns. I would love to some sort of syntactic sugar in C# to allow for this to happen. I am, however, encouraged that they are working with the F# team and other teams to ensure compatibility between the libraries.

If you open Reflector, you will find the type definitions in mscorlib.dll version 4.0 under the System namespace. You may also be surprised to find them as internal classes only at this point, which is unfortunate and we find ourselves not able to take advantage of these things such as the CodeContracts and BigInteger/BigNumber in the .NET 3.5 libraries.

As you can see from the above screen catpure, we have up to 7 arguments for a given tuple and the rest as defined by another tuple. I, however, haven't seen tuples quite that large before, but it's always possible...

The Zip Operator Function

Another functional programming item that has been added to the System.Linq.Enumerable class in System.Core.dll. This method allows us to combine two collections together using a function to calculate the new element given the element from each collection.

In F#, we have two ways of doing this in F# in the Seq module. They are defined as:

val map2 : ('a -> 'b -> 'c) -> seq<'a> -> seq<'b> -> seq<'c> 
  
val zip : seq<'a> -> seq<'b> -> seq<'a * 'b>

The map2 function takes a function which takes the two items from the list to produce the calculated item, and two collections and returns a new collection of the computed items. If one collection is shorter than the other, the rest of the computations are not completed. The zip function is a simple function which takes the items from the first and second collection and combines them in a tuple.

An example of each follows:

// Map2 
  
let l1 = seq[1 .. 26] 
  
let l2 = seq['a' .. 'z'] 
  
let mapped = Seq.map2  
  (fun a b -> sprintf "%d%c" a b) l1 l2 
  
// Zip 
  
let z1 = seq['a' .. 'z'] 
  
let z2 = seq['A' .. 'Z'] 
  
let zipped = Seq.zip z1 z2

Now, to use the C# version is rather simple. The signature of this method is simply:

public static IEnumerable<TResult> Zip<TFirst, TSecond, TResult>( 
  
  this IEnumerable<TFirst> first,  
  IEnumerable<TSecond> second,  
  Func<TFirst, TSecond, TResult> func)

As you can see, this follows the same exact pattern as the map2 function from F#, which allows us to compose the two items together via a function to compute the hew item. Let's define a few tests that will pass given our knowledge of the Zip function. We can also include the Tuple class, well, at least the F# version to show that behavior as well. These are basically tests that I wrote for my Functional C# library, but I hadn't published my tests, and I probably should.

[Fact] 
  
public void ZipWithAdding_ShouldAddRanges() 
  
{ 
  
    // Arrange 
  
    var range1 = Enumerable.Range(1, 10); 
  
    var range2 = Enumerable.Range(11, 10); 
  
    // Act 
  
    var range3 = range1.Zip(range2, (i, j) => i + j); 
  
    // Assert 
  
    Assert.True(range3.Count() == 10); 
  
    Assert.True(range3.ElementAt(0) == 12); 
  
    Assert.True(range3.ElementAt(9) == 30); 
  
} 
  
[Fact] 
  
public void ZipWithIntAndChar_ShouldCombine() 
  
{ 
  
    // Arrange 
  
    var range1 = Enumerable.Range(1, 5); 
  
    var range2 = new[] { 'a', 'b', 'c', 'd', 'e' }; 
  
    // Act 
  
    var range3 = range1.Zip(range2, (i, j) => i + j.ToString()); 
  
    // Assert 
  
    Assert.True(range3.Count() == 5); 
  
    Assert.True(range3.ElementAt(0) == "1a"); 
  
    Assert.True(range3.ElementAt(4) == "5e"); 
  
} 
  
[Fact] 
  
public void ZipWithTuples_ShouldCombineLists() 
  
{ 
  
    // Arrange 
  
    var range1 = Enumerable.Range(1, 5); 
  
    var range2 = new[] { 'a', 'b', 'c', 'd', 'e' }; 
  
    // Act 
  
    var range3 = range1.Zip(range2, (i, j) => new Tuple<int, char>(i, j)); 
  
    // Assert 
  
    Assert.True(range3.Count() == 5); 
  
    Assert.True(range3.ElementAt(0).CompareTo( 
  
        new Tuple<int, char>(1, 'a')) == 0); 
  
    Assert.True(range3.ElementAt(4).CompareTo( 
  
        new Tuple<int, char>(5, 'e')) == 0); 
  
}

Because the Parallel Extensions for .NET are becoming part of the BCL in .NET 4.0, the ParallelEnumerable also has the Zip method as well, which allows us to take advantage of data parallelism, should our machine allow such as this:

[Fact] 
  
public void ParallelZipWithAdding_ShouldAddRanges() 
  
{ 
  
    // Arrange 
  
    var range1 = ParallelEnumerable.Range(1, 10); 
  
    var range2 = ParallelEnumerable.Range(11, 10); 
  
    // Act 
  
    var range3 = range1.Zip(range2, (i, j) => i + j); 
  
    // Assert 
  
    Assert.True(range3.Count() == 10); 
  
    Assert.True(range3.ElementAt(0) == 12); 
  
    Assert.True(range3.ElementAt(9) == 30); 
  
}

With the including of the Parallel Extensions for .NET, it's going to be a lot of more functional fun built-into the BCL. I can only hope for more of this coming down the road.

Wrapping It Up

Although the .NET Framework 4.0 release didn't give too many items for functional programming as they had in the .NET 3.5 release, the .NET 4.0 Framework has a few interesting items with the inclusion of the Tuple and Zip method. Even more intrigue of course comes from adding the Parallel Extensions for the .NET Framework to the base class library as a first-class citizen.

I'd wish they would have made the Tuple class public already so that we could at least play around with some of those features, but I as many understand why some of the decisions were made, and I also realize it's early in the cycle still. Hopefully in the next release or so, it will become available to us to use, including some syntactic sugar about their creation and decomposition, but ultimately, that's a language decision and not necessarily a framework decision.

It's great to see a language convergence in terms of libraries now being available to all. F# will continue to be my language of choice, but with C# gaining some of these libraries, it makes the transition switch much easier without having to reinvent the wheel with either re-implementing the feature or converting Func delegates to F# FastFunc types and back again.

.NET Code Contracts and TDD Are Complementary

podwysocki — Fri, 14 Nov 2008 17:11:00 -0600

After my recent post on the introduction of Code Contracts in .NET 4.0, I got some strong reaction that they would rather rely on TDD, or the better term, Example Driven Development specifications to ensure correctness. Instead, it's my intent to talk about how they can complement each other in some rather powerful ways, such as having contracts bound to interfaces instead of class instances to ensure uniform interaction. When we combine these two things together, the edge cases of our behaviors quickly melt away.

Design by Contract Basics

In order to understand how it can help, it's best to understand more about what Design by Contract can do for us. The basic idea revolves around three questions:

What does it expect? (Pre-conditions)
What does it guarantee? (Post-conditions)
What does it maintain? (Invariants)

Now, to map that to actual software terms, these constraints are enforced at the method level. Listed below are the basic rules for how contracts work:

Pre-conditions may be weakened and not strengthened by subclasses
Post-conditions may be strengthened and not weakened by subclasses
Invariants may be strengthened and not weakened by classes

The intent of DbC and using contracts, your program must never try to verify the contract conditions and instead fail hard, with the contract verification being your safety net. This fail hard technique makes reading and understanding this code easier because the intended behavior is clearly specified. When using the .NET Code Contracts, these hard failures are enforced either through the Debug.Assert or the Environment.FailFast implementations, depending on the build configuration.

TDD and Contracts Strategies

We have a couple of options when we talk about Code Contracts and TDD. Either way, the tests always come first. Then what comes next is up to interpretation.

We have the option of:

Defining the contract implementation after the test, to narrow the behavior of the code under test, then write the code required to pass.
Defining the code to achieve a passing test, then refactor the code to a contract implementation.

It really depends on the application as to which style might work better. For most applications, I would recommend that you go with the second option where you define the code first to pass, and then refactor to an evolving contract design. For those creating frameworks with predefined behaviors, the first option would probably work best.

One thing that Code Contracts gives us is the ability apply intrinsic behavior to interfaces. At that point, I no longer really call them interfaces, but abstract contracts is a better term for them. I favor their use as much as possible to achieve uniform behavior across implementations and really becomes a powerful tool to enforce Don't Repeat Yourself (DRY).

Red - Yellow - Green Refactor

One analogy that can be adapted here is the original idea of Red, Green, Refactor. Let's take this a step further to use a phrase that Greg Young uses, which is Red, Yellow, Green, Refactor. This is to say that we first implement the test, fail with a red light because no code actually exists for it to compile or work. Then we implement the contract and our code to a point where it can at least compile, which would be yellow. After that, we then pass our test with green after implementing the right amount of code to satisfy our contract. We can refactor our contracts and code to clean it up a bit more, and move onto the next test.

BDD for the Business and DbC for the Minutia

Another argument that can be made is that we could make is that we treat BDD for the business and Design by Contract for the minutia. This idea is that we can continue to use the BDD syntax that we normally do, and then use contracts to enforce the edge constraints, to narrow our definitions. This would allow us to focus on the business at the high level using BDD, and then the low level enforcement using Code Contracts.

Domain Driven Design and Design by Contract

One of the topics mentioned in the hallmark book Domain Driven Design, Eric Evans covers Design by Contract in Chapter 10 on Supple Design. In this chapter, he states:

State post-conditions of operations and invariants of classes and aggregates. If assertions cannot be coded directly into your programming language, write automated unit tests fort them. Write them into documentation or diagrams where it its the style of the project's development status.

Seek models with coherent sets of concepts, which lead a developer to infer the intended assertions, accelerating the learning curve and reducing the risk of contradictory code.

What is interesting is that he talks about putting assertions into our code. Given that Code Contracts are available to us to use, we can take advantage of exactly what he states. These contracts then become part of the documentation of our code, with an intention revealing interface of what the behavior of this code is.

Further, he states:

Even though many object oriented languages don't currently support assertions directly, assertions are still a powerful way of thinking about a design. Automated unit tests can partially compensate for lack of language support. Because assertions are all in the term of states, rather than procedures, they make tests easy to write. The test setup puts the preconditions in place; then, after execution, the tests check whether the post-conditions hold.

Clearly stated invariants and pre- and post-conditions allow for a developer to understand the consequences of using an operation or object.... so it's important to find models that make sense to people as well as satisfying the needs of the application.

This states the case rather succinctly for using code contracts when the language supports them. Indeed, to be able to statically enforce these constraints and prove their success or failure is key. Enough though of the talk about DbC and Domain Driven Design, let's actually walk through an example of how to work these in conjunction together.

Walking Through an Example

Let's walk through a simple example to demonstrate how these two may work together. In this example, we will define an immutable generic list that is optimized for recursion. This implementation would be fairly similar to an implementation done by the F# team as part of the immutable collections. I'll be going into that a bit later in a different post.

The first example we want to give is for an empty list. For the success criteria for this example, we will say that for a given empty list, an is empty flag should be true, the length is 0, and there should be exceptional behavior for checking the list head and tail.

[Fact] 
  
public void EmptyList_ShouldBeEmpty() 
  
{ 
  
    // Act  
  
    IImmutableList<int> list = ImmutableList<int>.Empty; 
  
    // Assert  
  
    Assert.True(list.IsEmpty); 
  
    Assert.True(list.Length == 0); 
  
    Assert.Throws<ArgumentException>(

        () => { var i = list[0]; }); 
  
    Assert.Throws<InvalidOperationException>( 
  
        () => { var head = list.Head; }); 
  
    Assert.Throws<InvalidOperationException>( 
  
        () => { var tail = list.Tail; }); 
  
}

Now that the empty list example has been defined, let's actually work to implement the behavior through the use of a contract. We're going to follow the first option enumerated above on defining a contract first, and then create the code to implement the feature, because this is more of a framework piece than it is for any standard line of business application code. In order to create code contracts on interfaces, we need to create a ContractClass that contains our contracts and decorate our interface for it. I will have to define later a class that implements the code contract class.

In my test above, I need to define a few items on my interface for success, which is an empty flag, a length, the head and the tail of the list. Below is the definition of this interface.

[ContractClass(typeof(IImmutableList_Contract<>))]  
public interface IImmutableList<T> : IEnumerable<T>  
{  
    bool IsEmpty { [Pure] get; }  
    int Length { [Pure] get; }  
    T Head { [Pure] get; }  
    IImmutableList<T> Tail { [Pure] get; }  
    T this[int index] { [Pure] get; }  
}  

Once this is defined, we can now create our contract class. This must implement the IImmutableList<T> interface as well as mark it with an attribute stating that it is the contract class for the given interface. Each method in turn must be implemented with their given pre-conditions, post-conditions and invariants. Each method must also return the result from the comutation by using the CodeContract.Result<T>() method.

  
[ContractClassFor(typeof(IImmutableList<>))] 
  
internal sealed class IImmutableList_Contract<T> : IImmutableList<T> 
  
{ 
  
    public IEnumerator<T> GetEnumerator() 
  
    { 
  
        CodeContract.Ensures(IsEmpty ? 
  
            null == CodeContract.Result<IEnumerator<T>>() : 
  
            null != CodeContract.Result<IEnumerator<T>>()); 
  
        return CodeContract.Result<IEnumerator<T>>(); 
  
    } 
  
    System.Collections.IEnumerator System.Collections.IEnumerable.GetEnumerator() 
  
    { 
  
        return GetEnumerator(); 
  
    } 
  
    public bool IsEmpty 
  
    { 
  
        [Pure] 
  
        get { return CodeContract.Result<bool>(); } 
  
    } 
  
    public int Length 
  
    { 
  
        [Pure] 
  
        get 
  
        { 
  
            CodeContract.Ensures(0 <= CodeContract.Result<int>()); 
  
            return CodeContract.Result<int>(); 
  
        } 
  
    } 
  
    public T Head 
  
    { 
  
        [Pure] 
  
        get 
  
        { 
  
            CodeContract.Requires(!IsEmpty); 
  
            return CodeContract.Result<T>(); 
  
        } 
  
    } 
  
    public IImmutableList<T> Tail 
  
    { 
  
        [Pure] 
  
        get 
  
        { 
  
            CodeContract.Requires(!IsEmpty); 
  
            return CodeContract.Result<IImmutableList<T>>(); 
  
        } 
  
    } 
  
    public T this[int index] 
  
    { 
  
        [Pure] 
  
        get 
  
        { 
  
            CodeContract.Requires(!IsEmpty); 
  
            CodeContract.Requires(0 <= index && Length < index); 
  
            return CodeContract.Result<T>(); 
  
        } 
  
    } 
  
}

Now there is enough code to satisfy my preconditions. Moving onto the actual implementation, there is a bit of code required to get this code to pass. Let's implement the bare bones code that would be required to get the test to pass.

public abstract class ImmutableList<T> : IImmutableList<T> 
  
{ 
  
    public class _Empty : ImmutableList<T> { } 
  
    public class _Cons : ImmutableList<T> 
  
    { 
  
        public T _Head { get; internal set; } 
  
        public ImmutableList<T> _Tail { get; internal set; } 
  
        internal _Cons(T head, ImmutableList<T> tail) 
  
        { 
  
            _Head = head; 
  
            _Tail = tail; 
  
        } 
  
    } 
  
    private static IImmutableList<T> empty = 
  
        new _Empty(); 
  
    public static IImmutableList<T> Empty  
    { get { return empty; } } 
  
    public bool IsEmpty 
  
    { [Pure] get { return this is _Empty; } } 
  
    public int Length 
  
    { [Pure] get { return 0; } } 
  
    public T Head 
  
    { [Pure] get { return ((_Cons)this)._Head; } } 
  
    public IImmutableList<T> Tail 
  
    { [Pure] get { return ((_Cons)this)._Tail; } } 
  
    public this[int index] 
  
    { [Pure] get { return default(T) } } 
  
}

Now that we got enough code to compile, we have another problem when we run the tests? What is it? Well, our exceptional cases go away, because the system will fail hard should you violate them by either calling Debug.Assert or Environment.FailFast. Therefore, the test needs to be rewritten slightly to leave off those exceptional cases.

[Fact]  
public void EmptyList_ShouldBeEmpty()  
{  
    // Act   
  
    IImmutableList<int> list = ImmutableList<int>.Empty;  

  
    // Assert   
  
    Assert.True(list.IsEmpty);  
    Assert.True(list.Length == 0);  
}

Now the test, as written should compile and succeed. What we have gained here is quite a bit. With static proving, and the ability to encapsulate behavior in our interfaces, we have saved ourselves from DRY for subsequent implementations of this interface. Given the success of this, we are now able to move on to our next test which is when we have items in the list, we should have a head, a tail, not empty and a length of 10.

[Fact] 
  
public void NonEmptyList_ShouldShowProperCount() 
  
{ 
  
    // Arrange 
  
    var range = Enumerable.Range(1, 10); 
  
    // Act 
  
    IImmutableList<int> list =  
        ImmutableList<int>.FromIEnumerator(range.GetEnumerator()); 
  
    // Assert 
  
    Assert.True(list.Length == 10); 
  
    Assert.False(list.IsEmpty);

    Assert.True(list[0] == 1); 

    Assert.True(list.Head == 1); 
  
    Assert.True(list.Tail != null); 
  
}

As we define more tests or examples as we call them, we further refine the contract to include the proper bounds checks and add more functionality to the interface and to the list implementation. What's nice about this implementation is that our contracts don't litter our code, but instead are enforced at the interface level. That's not to say that we can't later on add more invariants, pre-conditions and post-conditions to our class implementations itself instead of the interface level.

Checked Exceptions All Over Again?

Some people may look at this and start to wonder if this is checked exceptions all over again. It's not for some simple reasons. First off, the code contract implementation does not force you to handle the exceptions in any way. Instead, when this becomes part of the documentation, it states what the pre-conditions, post-conditions, and invariants are, and during compilation, they will be displayed back as warnings when you have violated the contracts, as well at runtime as hard failures. In the Java world, you are forced to handle the exceptions, even if you met the pre-conditions, which isn't very helpful.

Wrapping It Up

We have covered quite a bit here today. I hope this overview can give you a brief understanding of how Design by Contract can work in conjunction with TDD to produce verifiable code. Given the ability to statically verify our contracts and behavior is important as our contracts then become part of the documentation for our system. In the next post in this series, we're going to talk more about guidance on where you should compromise and where you should never compromise when it comes to Code Contracts.

In the mean time, as always, download the latest version of the .NET Code Contracts and give the team feedback.

KaizenConf'08 Functional Programming Presentation Video

podwysocki — Wed, 12 Nov 2008 19:19:00 -0600

Last week, I provided a basic wrap up of my functional programming talk at the Continuous Improvement in Software Development conference (KaizenConf) in Austin. Little did I realize that I was indeed being filmed while I talked by Mark Leon Watson. So, without further ado, enjoy the first 20 minutes of my talk. I should emphasize though that it's not the official position that designers will never be there, but instead, it's not the highest priority. In time, they may come as needs arise.

In this section of the talk, I cover the following areas:

What is Functional Programming?
Why does it matter?
How do we do it?
Functional C#, what parts are functional and what parts aren't
What is F# and why is it useful?

Functional Programming - Is it a Game Changer? (Part 1 - KaizenConf '08 Workshop) from Mark Leon Watson on Vimeo

Thanks to Mark and I hope you all enjoy and feedback would be appreciated. I haven't yet made my F# samples available, but as always, my C# ones are available at the Functional C# library on MSDN Code Gallery. More will be added there shortly to reflect some of the things I talked about here in the slides.

TODO: Email Scott Lock

Code Contracts for .NET 4.0 - Spec# Comes Alive

podwysocki — Fri, 07 Nov 2008 23:40:00 -0600

As I've said in many posts before, I'm a big fan of stating your preconditions, postconditions, invariants and so on explicitly in your code through the use of contracts in the Design by Contract Parlance. Spec# is a project that came from Microsoft Research as a language based upon C# to add Design by Contract features to the language. I've talked extensively on the subject in the past on this blog and previous blogs of mine especially around the time of the ALT.NET Open Spaces, Seattle event back in April of this year. The importance of making side effects well known is something that I mentioned briefly during my Approaching Functional Programming talk at KaizenConf. To be able to express and statically verify behavior is important in regards to side effects and method purity.

One of the less talked about items from this year's Professional Developer Conference was Code Contracts for .NET. This talk was bundled in with automated test generation with Pex for a combined talk called "Research: Contract Checking and Automated Test Generation with Pex". In this talk, Mike Barnett, of the Spec# team was joined by Nikolai Tillmann, who is currently leading the Pex Project, and they talk about the project, Code Contracts for .NET. I encourage you to watch the video to see how it works and the benefits of using the library. It's been rewarding to watch how Spec# has grown in presence in recent months, especially the publicity that both Greg Young and I have given them. Mike has done a great job with this project and I'm really excited for the future of it.

Code Contracts for .NET

It was announced that a subset of Spec#, the contracts library, would be included as part of the base class library in .NET 4.0. When .NET 3.5 came out, if you opened System.Core.dll through .NET Reflector, you may have noticed that there was a namespace in there called Microsoft.Contracts. Since that time, the Spec# team has worked with the Base Class Library team to help integrate this more thoroughly into the libraries as a language agnostic approach. There are many decisions to be made as languages and frameworks evolve as to what goes where. To make these features as library features allows for more rapid change and flexibility than if they were exclusive language constructs such as they were with Spec#. After all, I want to be able to switch to languages such as F# and still have the ability to statically verify my code.

First things first, what is Design by Contract? It's an approach to software development that was coined by Dr. Betrand Meyer through the creation of the Eiffel language. The main tenets of this paradigm include:

What does it expect? (Preconditions)
What does it guarantee? (Postconditions)
What does it maintain? (Invariants)

The idea is to have these tenets enforced programmatically through the language itself. To this end, in the .NET framework, outside of Spec#, haven't had this available to them. So, the Spec# team realized, that instead of the language approach, maybe they should focus on a language agnostic approach through the use of libraries, and static verification. Now, I can feel free to use my language of choice inside the .NET framework to utilize these contracts, such as F#, C#, VB, etc. As part of the release at PDC, we have the libraries available to us for use in Visual Studio 2008, so we'll be going through what exactly that means.

Getting Started

First, you need to install the Code Contracts for .NET, which you can find here. This integrates with Visual Studio 2008 and adds an additional property window to your project files. This gives us the ability to enforce contracts using the Microsoft.Contracts.dll. If you look at the property page for your given project, it should look like this.

As you can see, we have the ability to perform runtime checking, static contract checking with non-null obligations and array bounds automatically. The install comes with a PDF with some documentation on how to use the library when covering preconditions, postconditions, invariants, purity and contract classes. Let's go through a quick example of using this library.

Using the Library

In order to utilize contracts, you must use the CodeContract class from the System.Diagnostics.Contracts namespace. The CodeContract has a few interesting methods worth exploring.

Method	Meaning
Assert	Express contract assertions
Assume	Express contract assumptions that should hold. Assume to be true or false
EndContractBlock	Used to mark the end of a code contract block of if statements
Ensures	Express postconditions
EnsuresOnThrow	Express postconditions that abnormally terminate a method
Exists	Ensure a value exists in a collection
ForAll	Express constraint for each item in a collection
Invariant	Express invariant constraints
OldValue	Retrieve the old value from the pre-state
Requires	Express preconditions
RequiresAlways	Express preconditions for all build configurations
Result	Get the method's return value
Throws	Express exceptional postcondition
ValueAtReturn	Specify out parameter value for postcondition checking

There are several attributes worth noting as well in this library as well:

Attribute	Meaning
ContractClassAttribute	Define a code contract class used to enforce contracts on an interface
ContractClassForAttribute	Define a code contract class for a given interface
ContractInvariantMethodAttribute	Used to mark a method that represents the object invariant
ContractPublicPropertyNameAttribute	Used in a method contract where the method is more visible than the field
ContractVerificationAttribute	Used to assume correctness of the given assembnly
PureAttribute	Express method purity
RuntimeContractAttribute	Added to the assembly via the rewriter to express that is has already been rewritten

As you can see here, we have a lot of goodies in here. Let's step just through preconditions for right now.

Preconditions

The first item we noted in our definition of Design by Contract is what do we expect. In this example, let's create a simple Geocoordinate value object used to hold latitude and longitude values. There are some constraints we need to use to ensure correctness. We need to enforce preconditions on the constructor as well as a function used to calculate the distance between two Geocoordinate classes. Since I want this available in all build configuration, I will use the CodeContract.RequiresAlways method to define my precondition contracts.

Let's take a look at what that might look like:

public class Geocoordinate 
  
{ 
  
    private readonly double latitude; 
  
    private readonly double longitude; 
  
    public Geocoordinate(double latitude, double longitude) 
  
    { 
  
        CodeContract.RequiresAlways(latitude <= 90.0 && latitude >= -90.0); 
  
        CodeContract.RequiresAlways(longitude <= 180.0 && longitude >= -180.0); 
  
        this.latitude = latitude; 
  
        this.longitude = longitude; 
  
    } 
  
    [Pure] 
  
    public double Latitude { get { return latitude; } } 
  
    [Pure] 
  
    public double Longitude { get { return longitude; } } 
  
    [Pure] 
  
    public static double GetDistance(Geocoordinate g1, Geocoordinate g2) 
  
    { 
  
        CodeContract.RequiresAlways(g1 != null); 
  
        CodeContract.RequiresAlways(g2 != null); 
  
        const double R = 3956; 
  
        const double degreesToRadians = Math.PI / 180; 
  
        var lon1 = g1.Longitude * degreesToRadians; 
  
        var lat1 = g1.Latitude * degreesToRadians; 
  
        var lon2 = g2.Longitude * degreesToRadians; 
  
        var lat2 = g2.Latitude * degreesToRadians; 
  
        var dlon = lon2 - lon1; 
  
        var dlat = lat2 - lat1; 
  
        var a = Math.Pow(Math.Sin(dlat / 2), 2) + Math.Cos(lat1) * Math.Cos(lat2) * Math.Pow(Math.Sin(dlon / 2), 2); 
  
        var c = 2 * Math.Atan2(Math.Sqrt(a), Math.Sqrt(1 - a)); 
  
        var d = R * c; 
  
        return d;  
    } 
  
}

I also added method purity just for clarity sake. This allows me to specify that I am not changing object state, and is quite useful for enforcement. This makes it obvious to the caller that this method does no more than compute the result and return it. That's important and reassuring when using third party libraries. Let's say I call this class with the following code:

static void Main(string[] args) 
  
{ 
  
    var g = new Geocoordinate(91.0, 181.0); 
  
    var g1 = new Geocoordinate(40.774, 73.972); 
  
    var g2 = new Geocoordinate(40.811, 73.910); 
  
    var distance = Geocoordinate.GetDistance(g1, g2); 
  
    Console.WriteLine(distance); 
  
}

You may notice that the g is out of bounds from my precondition. When I run the application, I get a nasty reminder that I broke the contract.

That's exactly the behavior we wanted to express through our precondition. There is a lot more to cover in subsequent posts on the subject, but I hope this gives you a sense of some of the power of the library.

Wrapping It Up

This is just a first look at the new Code Contracts library. In my talks at the Continuous Improvement in Software Development conference, I stressed the need to for our intentions to be more clear in our code. This is a great first step to creating a language agnostic approach to static code verification. To be able to ensure to the caller what the API will expect, return and maintain is especially powerful and I think important in the future of software development, especially in regards to state management. The language agnostic approach given with this library is an important step forward, so that I could statically verify my code no matter the language on the .NET platform. There is a lot more to this library to explore. I urge you to download it, and give them feedback. You can post feedback on the Pex forums or send them an email at codconfb _at_ microsoft _dot_ com.