Not only is the new Pex actually compatible with the recently-​​released VS 2010 RC, it also sports a few new features and bug fixes.

Check out the Release Notes and Download this puppy today!

If you need some visuals on Pex, check out this excellent video (which demon­strates Pex in Visual Studio 2008).

Enough said.

EMC2, who took over Conchango, has made available a Release Candidate version of their Scrum templates for Team Foundation Server 2010 RC.

The download consists of a Scrum Masters' Workbench desktop utility and the actual process template. I'll be eval­u­ating this soon, so expect a "first impres­sions" review here on my blog in a week or two. I'm espe­cially inter­ested to see how it compares to the MSF-​​Agile 5 template, since Microsoft has revamped it to be (much) more like Scrum.

I've used Scrum for Team System 2008 about a year ago and was quite happy with it.

As in Brad Abrams' Framework Design Guidelines [Amazon][Barnes & Noble], which docu­ments coding and naming conven­tions for .NET, we need coding conven­tions for the new Code Contracts feature. What are yours?

These are mine:

DO use pre– and post­con­di­tions on all methods, public and private.

DO prefer to write contracts on inter­faces, then on abstract classes, then on concrete classes.

DO specify ArgumentNullException for non-​​null input parameters.

DO specify ArgumentOutOfRangeException for input para­meters that have to be within a certain
range.

DO specify post­con­di­tions, when possible, on functions.

   1:  public string NoSpacesAnywhere(string input, int range)

   2:  {

   3:      Contract.Requires<ArgumentNullException>(!string.IsNullOrEmpty(inpu

   4:      t));

   5:      Contract.Requires<ArgumentOutOfRangeException>(range < 0 || range >

   6:      100);

   7:      Contract.Ensures(Contract.Result<string>() != null);

   8:      …

   9:  }

DO write object invariant methods on classes that have prop­erties, even if they are not public. Write the invariants on the place­holder fields instead of on the prop­erties them­selves. This guar­antees that even if a method tries to be “clever” by updating a place­holder field directly, which it should not do, the condi­tions are still checked.

   1:  [ClassInvariantMethod]

   2:  void ObjectInvariant()

   3:  {

   4:      Contract.Invariant(_age >= 16);

   5:      Contract.Invariant(!string.IsNullOrEmpty(_name));

   6:      …

   7:  }

DO write pre– and post­con­di­tions on prop­erties, unless you use auto­matic prop­erties. In that case, you must just write the condi­tions in the invariant, and they will auto­mat­i­cally be compiled into the property code.

In fact, it installs without problems, but when trying to run it, you get an incom­pat­i­bility issue.

I hear that version 0.23 will support the RC, so I guess we'll have to wait. I hope they'll release 0.23 very soon, because Pex + Code Contracts = Rock 'n Roll!

If you use ReSharper, you get warnings in your code editor whenever ReSharper's static checker thinks you might be accessing a null object. However, if you have just spec­ified a Contract.Requires(x != null) then ReSharper still complains about a possible use of null.

Ring a bell?

Luckily we can solve this. John Gietzen has a post up on Stack Overflow about using ReSharper XML files to "teach" ReSharper to recognize when an object has been tested for null already.

Thanks John, and thanks Hakim for pointing this out to me!

Yes!! Yesterday (Monday, February 8^th, 2010), Microsoft made Visual Studio 2010 RC and .NET Framework 4 RC available to MSDN Subscribers.

Tomorrow, the whole world will be able to enjoy the Release Candidate versions of this software — including Team Foundation Server 2010 RC — as down­loads on the MSDN public website.

UPDATE: Visual Studio 2010 RC is FAST!! And if you'd been using the Beta 2 with the latest Beta of ReSharper 5, then there's more good news: the latest nightly build of ReSharper works great with Visual Studio 2010 RC!

(via MSDN)

Earlier, I blogged about Code Contracts as a tool to help you specify and verify code behavior. Today let's have a closer look with a prac­tical example.

Say that we need to create a new class, a priority queue. We write the spec­i­fi­cation of the new class, natu­rally, as an interface to implement:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33

namespace AdvancedCodeContracts
{
	/// <summary>
	/// Interface for priority queue classes.
	/// </summary>
	/// <typeparam name="T">Item type.</typeparam>
 
	public interface IPriorityQueue<T> where T : class
	{
		/// <summary>
		/// Gets the number of items in the queue.
		/// </summary>
		int Count { get; }
 
		/// <summary>
		/// Enqueues a new item with a priority (higher is better).
		/// </summary>
		/// <param name="priority">Priority between 1 and 100.</param>
		/// <param name="item">Item to enqueue.</param>
		void Enqueue(int priority, T item);
 
		/// <summary>
		/// Dequeues the item with the highest priority.
		/// </summary>
		/// <returns></returns>
		T Dequeue();
 
		/// <summary>
		/// Clears the queue.
		/// </summary>
		void Clear();
	}
}

This is a straight­forward, plain-​​vanilla priority queue as I'm sure we've all written at one stage or another. It is, of course, a Best Practice to imme­di­ately document the interface.

Now, can we already define what constraints to put on the implementation(s) of this interface? That is, can we write, per method and property, a set of pre– and post­con­di­tions that must be satisfied? Can we write an object invariant for the class?

Of course we can. We can also write unit tests for it. After all, we are all doing Test-​​Driven Development, aren't we?

So we must make a choice: either we write the contracts first, or the unit tests.

I think this choice is a matter of personal pref­erence. You have to write both before you do the imple­men­tation anyway… OK, true, you don't really have to, but it's a Best Practice to write code contracts before imple­men­tation, and it's another Best Practice to write unit tests before imple­men­tation. Why? Just because.

No, because this saves valuable devel­opment time as it cuts short debugging. It forces us as devel­opers to think about our approach before we start hacking away at the code.

OK, then, let's do those code contracts first.

But we don't have an imple­men­tation yet! So how do we approach this?

We can actually specify a code contract on an interface. Think inher­i­tance: all classes that implement the interface, inherit the code contract and thus must satisfy it. They can also extend the contract by adding extra post­con­di­tions to methods (not precon­di­tions) and extra object invariants. How cool is that?

So let's add a code contract to the interface. We start by adding a using and an attribute to the interface:

1
2
3

using System.Diagnostics.Contracts;
 
[ContractClass(typeof(IPriorityQueueContract<>))]

As you would imagine, this tells the compiler that there exists a class called IPriorityQueueContract that imple­ments a code contract on this interface. Notice the absence of the T in the attribute, though; you cannot use that syntax in an attribute, so you have to leave the generic T out. Believe it or not, this actually compiles, and it works, too.

Incidentally, if you are using .NET 4.0, you don't need to add any refer­ences to your project. The System.Diagnostics.Contracts name­space is included in mscorlib. But if you're old-​​school (still working with .NET Framework 3.5), you'll need to download the Code Contracts library and reference it.

OK, fine. Problem is of course that we don't have that class yet, so we create it:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

using System;
using System.Diagnostics.Contracts;
 
namespace AdvancedCodeContracts
{
  [ContractClassFor(typeof(IPriorityQueue<>))]
  public class IPriorityQueueContract<T> : IPriorityQueue<T> where T : class
  {
    public int Count
    {
      get
      {
        return 0;
      }
    }
 
    public void Enqueue(int priority, T item)
    {
    }
 
    public T Dequeue()
    {
      return (T)new object();
    }
 
    public void Clear()
    {
    }
  }
}

It is my habit to call contract classes simply Contract. That is the convention I use, but you may have a policy against classes having names that start with I.

In this class, we specify that this is a contract class for the IPriorityQueue interface, and we actually implement that interface. That is why the Count property and the Dequeue() method are actually returning values; because we must implement the interface. The values that this class returns are irrel­evant and are ignored by the Code Contracts system.

Let's fill in the pre– and post­con­di­tions and the object invariant now:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47

using System;
using System.Diagnostics.Contracts;
namespace AdvancedCodeContracts
{
 
  [ContractClassFor(typeof(IPriorityQueue<>))]
  public class IPriorityQueueContract<T> : IPriorityQueue<T> where T : class
  {
    [ContractInvariantMethod]
    void ObjectInvariant()
    {
      Contract.Invariant(this.Count >= 0);
    }
 
 
    // dummy implementation, we don't need a contract here
    public int Count
    {
      get
      {
        return 0;
      }
    }
 
 
    public void Enqueue(int priority, T item)
    {
      Contract.Requires<ArgumentOutOfRangeException>(priority >= 1 && priority <= 100);
      Contract.Requires<ArgumentNullException>(item != null);
      Contract.Ensures(this.Count == Contract.OldValue(this.Count) + 1);
    }
 
 
    public T Dequeue()
    {
      Contract.Requires<InvalidOperationException>(this.Count > 0);
      Contact.Ensures(Contract.Result<T>() != null);
      Contract.Ensures(this.Count == Contract.OldValue(this.Count) - 1);
      return (T)new object();
    }
 
 
    public void Clear()
    {
      Contract.Ensures(this.Count == 0);
    }
  }

In the object invariant, we say that the Count property must always return a positive number. Because we do so, we do not need to specify this again as a post­con­dition in the property itself.

The Enqueue() method lays down two preconditions:

• The priority para­meter must be between 1 and 100, inclusive;
• The item to enqueue may not be null.

The method further spec­ifies a post­con­dition that stip­u­lates that the Count property is increased by 1; so at the end of the method, the new value of Count must be the old value + 1. Note that currently, the Contract.OldValue() method is only valid inside a Contract.Ensures().

Next, we define a single precon­dition on Dequeue(): the queue may not be empty. We throw an InvalidOperationException if it is. We also specify two post­con­di­tions for this method:

• The result is never null. We can guar­antee this because we don't allow enqueing null in the first place.
• The Count property is always decreased by 1.

Finally, the Clear() method guar­antees, by means of a single post­con­dition, that the queue will be empty.

Are we having fun yet?

Note that all condi­tions in the code contract use public prop­erties or input para­meters only. There is no reference to any private vari­ables. This is logical even if the code contract is not just defined on an interface; it is a code contract after all, so its details must be visible outside of the implementation.

This code can compile, even though we don't have a concrete imple­men­tation of our priority queue yet.

So let's write a set of unit tests. Let's throw every­thing we can think of right now at that interface:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80

using System;
using AdvancedCodeContracts;
using Microsoft.VisualStudio.TestTools.UnitTesting;
 
namespace AdvancedCodeContractsBlackboxTests
{
  [TestClass]
  public class PriorityQueueOfStringUnitTests
  {
    private IPriorityQueue<string> sut;
 
    [TestInitialize]
    public void TestInitialize()
    {
      sut = new PriorityQueue<string>();
    }
 
    [TestMethod]
    public void PriorityQueue_InitialState_Ok()
    {
      Assert.IsNotNull(sut);
      Assert.AreEqual(0, sut.Count);
    }
 
    [TestMethod]
    public void PriorityQueue_AddSingleItem_CountIs1()
    {
      sut.Enqueue(1, "This is one");
      Assert.AreEqual(1, sut.Count);
    }
 
    [TestMethod]
    public void PriorityQueue_AddSingleItemAndDequeue_Ok()
    {
      sut.Enqueue(1, "This is one");
      string result = sut.Dequeue();
      Assert.AreEqual(0, sut.Count);
      Assert.AreEqual("This is one", result);
    }
 
    [TestMethod]
    [ExpectedException(typeof (InvalidOperationException))]
    public void PriorityQueue_DequeueFromEmptyQueue_ThrowsInvalidOperationException()
    {
      string result = sut.Dequeue();
    }
 
    [TestMethod]
    [ExpectedException(typeof (ArgumentNullException))]
    public void PriorityQueue_EnqueueNull_ThrowsArgumentNullException()
    {
      sut.Enqueue(1, null);
    }
 
    [TestMethod]
    [ExpectedException(typeof (ArgumentOutOfRangeException))]
    public void PriorityQueue_EnqueuePriority0_ThrowsArgumentOutOfRangeException()
    {
      sut.Enqueue(0, "dummy");
    }
 
    [TestMethod]
    [ExpectedException(typeof (ArgumentOutOfRangeException))]
    public void PriorityQueue_EnqueuePriority101_ThrowsArgumentOutOfRangeException()
    {
      sut.Enqueue(101, "dummy");
    }
 
    [TestMethod]
    public void PriorityQueue_Clear_Ok()
    {
      sut.Enqueue(1, "One");
      sut.Enqueue(1, "Two");
      sut.Enqueue(1, "Three");
      sut.Clear();
 
      Assert.AreEqual(0, sut.Count);
    }
  }
}

Yes, the unit tests are written against an interface (IPriorityQueue). We do assume that we'll write a concrete class called PriorityQueue. We'll do that as the next step.

But first, let's look at these tests. They are of course quite straight­forward. Any class that satisfies these tests can right­fully be called a priority queue, even though in the TestInitialize() method, we instan­tiate our subject under test (sut) as an instance of the PriorityQueue class.

Convention Alert: I use the test naming convention _​_​. I find it makes for readable unit test code as well as readable test lists. Again, your mileage may vary.

Let's add a couple more tests just for fun:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47

[TestMethod]
public void PriorityQueue_AddMultiplePrioritizedItemsAndDequeue_Ok()
{
  sut.Enqueue(1, "This is one");
  sut.Enqueue(2, "This is two");
  sut.Enqueue(5, "This is three");
  sut.Enqueue(3, "This is four");
  sut.Enqueue(4, "This is five");
  Assert.AreEqual(5, sut.Count);
 
  string result;
  result = sut.Dequeue();
  Assert.AreEqual(4, sut.Count);
  Assert.AreEqual("This is three", result);
 
  result = sut.Dequeue();
  Assert.AreEqual(3, sut.Count);
  Assert.AreEqual("This is five", result);
 
  result = sut.Dequeue();
  Assert.AreEqual(2, sut.Count);
  Assert.AreEqual("This is four", result);
 
  result = sut.Dequeue();
  Assert.AreEqual(1, sut.Count);
  Assert.AreEqual("This is two", result);
 
  result = sut.Dequeue();
  Assert.AreEqual(0, sut.Count);
  Assert.AreEqual("This is one", result);
}
 
[TestMethod]
public void PriorityQueue_EnqueueMultipleItemsWithSamePriority_Ok()
{
  sut.Enqueue(1, "One");
  sut.Enqueue(1, "Two");
  sut.Enqueue(1, "Three");
  Assert.AreEqual(3, sut.Count);
}
 
[TestMethod]
public void PriorityQueue_ClearOnEmptyQueue_Ok()
{
  sut.Clear();
  Assert.AreEqual(0, sut.Count);
}

Uh, those tests are actually necessary – not just fun. Good that we caught them before we started writing "real" code.

OK, now we're ready to actually write the implementation.

In case you've never done TDD before: how do you feel right now? Don't you feel pretty sure that whatever we'll come up with as code will be tested very well? And what are the odds that we'll come up with working code quickly, without too much "red" in our unit test results?

Here's a concrete, if simple, implementation:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52

using System.Collections.Generic;
using System.Diagnostics.Contracts;
using System.Linq;
 
namespace AdvancedCodeContracts
{
  public class PriorityQueue<T> : IPriorityQueue<T> where T : class
  {
    private List<Item> _list = new List<Item>();
 
    public int Count
    {
      get { return _list.Count; }
    }
 
    public void Enqueue(int priority, T toEnqueue)
    {
      Item item = new Item { Priority = priority, Object = toEnqueue };
      _list.Add(item);
    }
 
    public T Dequeue()
    {
      int highest = _list.Max(i => i.Priority);
      Item item = _list.First(i => i.Priority == highest);
      _list.Remove(item);
      return item.Object;
    }
 
    public void Clear()
    {
      _list.Clear();
    }
 
    [ContractInvariantMethod]
    void SpecificObjectInvariant()
    {
      Contract.Invariant(_list != null);
    }
 
    #region Nested type: Item
 
    private class Item
    {
      public int Priority { get; set; }
 
      public T Object { get; set; }
    }
 
    #endregion
  }
}

This is a correct imple­men­tation. How do I know? Because all unit tests run and the code contract is satisfied – otherwise at least one pre– and/​or post­con­dition and/​or object invariant would have failed.

Did you notice that this concrete imple­men­tation adds post­con­di­tions and a more specific object invariant to the contract? This is allowed because specific imple­men­ta­tions may offer extra output guar­antees (post­con­di­tions), and may include specific (read: private field/​property) invariants. Extra precon­di­tions are not allowed; as we inherit from a public interface or even a concrete imple­men­tation, we may not narrow the contract.

Next, we may modify the code for more perfor­mance, or better yet, write another imple­men­tation (say, a FastPriorityQueue) that imple­ments the same interface, and therefore the same code contract, and therefore – with one small change in TestInitialize() – the same unit tests.

Good code docu­ments and verifies itself. Code Contracts are the way to do it. Will they be part of your team's Quality Assurance arsenal too?

If you'd like to start a new project using Team Foundation Server 2010 Beta 2 now, you might wonder whether this is a good idea. Microsoft has announced that there will be a public RC of both Visual Studio 2010 and Team Foundation Server 2010 "soon" (mid-​​February is my best guess; RTM is set for April 12).

However, it will be possible to upgrade smoothly from the Beta 2 software to the RC and even to the RTM — including TFS. As I under­stand it from this post on MSDN, the database format of TFS Beta 2 and RC/​RTM will not change, and so the upgrade will be primarily a matter of unin­stalling Beta 2 and installing RC, if you follow proper procedure.

Nice!

What if there was a quick and easy way to double the power of unit tests, even hands-​​on tests?

Precursor: The Vienna Development Method

Many years ago at university in the Software Engineering class, the professor discussed the Vienna Development Method (VDM). This was a method to formally specify software and prove the integrity of a design.

Among other rules, VDM spec­ified that, per type of entity (i.e., per class) in the design, you can specify an object invariant. This is a set of condi­tions which must be true at any time inside every instance of the class. For example, you may specify that in an Account class, the Balance property must always be at least as high as the MinimumBalance property.

Another rule spec­ified that, per method (or "procedure"), you need to specify precon­di­tions and postconditions:

• A precon­dition is a condition which must always be true when the method starts executing.
• A post­con­dition is a condition that must always be true at the end of the method execution.

Typical examples of precon­di­tions are input para­meter vali­da­tions (such as amount > 0, amount <= MaxAmount, etc.), the fact that the object must already be initialized, etc.

Typical post­con­di­tions are: state is updated, the value returned from a function is not null or inside a given range, etc.

VDM, being a formal method after all, used a math­e­matical expression language to specify these condi­tions and invariants. You could then use math­e­matical methods to "prove" that these condi­tions were met, and that therefore the program was correct. Now, it's a far cry to assume that, if pre– and post­con­di­tions and invariants are indeed always met, the program must be correct. Still, I thought VDM was a valuable spec­i­fi­cation and devel­opment tool.

Much to my chagrin, in the following years I discovered that virtually nobody in the industry had ever heard of VDM or was even inter­ested in applying it! (This was one of my first expo­sures to the sad, sad state of profes­sional software devel­opment, but that's another story).

I did manage to sneak in pre– and post­con­di­tions in C and C++ code by using the assert() function, and later in C# using Debug.Assert(). It did the job, but better stuff was to come.

VDM Comes Alive

Fast-​​forward to 2007. Microsoft Research (MSR) creates Spec#, a superset of C# that adds code contracts to the .NET Framework 3.5. The MSR team is not the first to take VDM's prin­ciples and put them in code; the Eiffel language and the Java Modeling Language (JML) already exist.

Now, in 2009/​2010, they are making this cool stuff available to any CLR-​​based language under the name "Code Contracts".

Here's a simple example:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19

///
/// Gets the total value of the order, before rebates
/// and taxes.
///
public decimal TotalValue
{
    get
    {
        Contract.Requires(this.Lines != null);
        Contract.Ensures(Contract.Result() >= 0);
 
        decimal result = Lines
                .Where(x => x != null)
                .Sum(x => x.NumberOfItems * x.PricePerItem);
        Contract.Assume(result >= 0);
 
        return result;
    }
}

Contract.Requires spec­ifies a precondition.

Contract.Ensures spec­ifies a post­con­dition. Notice that the postcondition(s) are placed together with the precon­di­tions, which keeps things quite clear and readable, much more so than JML, in my opinion.

Now, you don't use code contracts just for declaring spec­i­fi­ca­tions. At runtime, and – here's the kicker – even at compile time, the Code Contracts system can use a static checker to verify the validity of the condi­tions and invariants. This is, therefore, not just a good help to translate spec­i­fi­ca­tions to code, but also to prove that these specs are met. Code Contracts are a great way to complement unit tests – in fact, all condi­tions are eval­uated during your unit tests too, rein­forcing their value.

Contract.Assume, as in the example above, spec­ifies an assumption; this is like an assertion, but weaker. At runtime there is no difference between an assumption and an assertion, but at compile-​​time the static checker will try to prove any assertion and generate a warning if it cannot. Since in the case above the static checker cannot prove that the result will be positive, we instruct the checker to assume that it is so. At runtime, the condition will still be checked and a contract exception will be thrown if it is not met.

Here's another simple example, this time of a contract invariant method:

1
2
3
4
5
6

[ContractInvariantMethod]
void ObjectInvariant()
{
    Contract.Invariant(Lines != null);
    Contract.Invariant(TotalValue >= 0);
}

In the coming days, I will post more examples and tech­niques for making the most of code contracts in .NET.