The Team Foundation Server team has just released the first beta of an all-​​new Scrum template for TFS 2010. This template competes with MSF Agile 5 up to some point, but more specif­i­cally it competes with EMC2's Scrum for Team System v3.

My first impression is that the new Scrum template is indeed a much better match for Scrum than MSF Agile 5, which was also targeted towards Scrum teams. It seems a simpler imple­men­tation than EMC2's (formerly Conchango's) template. Both are free.

Right now I am using EMC2's template on a project, and my client is about to roll out TFS 2010 on a larger scale, so for me the timing is just right. The next few weeks, we'll have a look at the new template and decide what to use for the next batch of projects.

It will be inter­esting to see whether Scrum teams every­where will adopt the more powerful Scrum for Team System v3 or will prefer the simpler, but less powerful, "standard" Microsoft imple­men­tation. Time will tell. I'd be most inter­ested to hear from you what you prefer, and why.

If you want to install TFS 2010 on a single-​​server instal­lation, be advised that Microsoft deter­mined that the minimum amount of available RAM should be 2 GB (it was 1 GB with the Beta and RC versions).

Microsoft's own research has shown that over 50% of all single-​​server instal­la­tions of the Release Candidate of TFS 2010 is on machines with less than 2 GB of RAM. These machines have to increase their memory before upgrading to RTM, or the new installer refuses to install.

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!

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.