Making Spec# a Priority
Spec# at ALT.NET Open Spaces, Seattle
As I said before I took a bit of time during Saturday to spend some time with the Spec# guys. I spent much of the morning with them in the IronRuby session explaining dynamic languages versus static ones. They had the session at 11:30, the second session of the day, in direct competition with the Functional Programming talk I had planned with Dustin Campbell. Greg was nice enough to record much of the session on a handheld camera and you can find that here. It's not the best quality, but you can understand most of it, so I'm pretty happy.
The things that were covered in this session were:
- Spec# overview
- Non-null Types
- Preconditions
- Postconditions
- Invariants
- Compile-Time checking versus Runtime checking
- Visual Studio Integration
Scott Hanselman also recorded a session with the Spec# guys for Episode 128. This is a much better interview than on DotNetRocks Episode 237 that Rustan did last year. This actually gets into the technical guts of the matter in a much better way, so go ahead and give it a listen. I was fortunate enough to be in the room at the time to listen.
The New Release
Mike and Rustan recently released a new version of Spec# back on April 11th so now Visual Studio 2008 is supported. You must remember though, this is still using the Spec# compiler that's only C# 2.0 compliant. So, anything using lambdas, extension methods, LINQ or anything like that is not supported. As always, you can find the installs here.
As with before, both the Spec# mode (stripped down mode) and C# mode are supported. What's really interesting is the inferred contracts. From an algorithm that Mike and Rustan worked on, they have the ability to scan a method to determine its preconditions and postconditions. It's not perfect, but to have that kind of Intellisense is really powerful.
What you can see is that the GetEnumerator method ensures that the result is new. Keep in mind, result is a keyword which states what the return value is for a method. It also says that the owner of IEnumerator will be the same as before. Object ownership is one of the more difficult things to comprehend with Spec# but equally powerful.
Another concept that's pretty interesting is the ability to make all reference types non-null by default in C# or in Spec# modes. Instead of having to mark your non-null types with an exclamation mark (!), instead you can mark your nullable types with a question mark (?) much as you would with the System.Nullable<T> generic class. All it takes is the flip of a switch in Spec#:
Or in the C# mode:
And then you have all the Spec# goodness.
Why It's Important
So, why have I been harping on this? To be able to express DbC as part of my method signature is extremely important to me. To be able to express my preconditions (what I require), postconditions (what I ensure), my invariants (what state will change) is a pretty powerful concept. Not to mention, to enforce immutability and method purity is also a pretty strong concept, especially in the times of multi-core processing. More on that subject later.
Focus on Behaviors
What Spec# can bring to the table is the ability to knock out a bit of your unit tests. Now, I don't mean all of them, but what about the ones that check for null values? Are they valid if you already put in your method signature to require a non-null value or use the ! symbol to denote a non-null type? Those edge cases aren't really valid anymore. The ability to track your invariants is the same as well as your postconditions. Instead, what that does is frees you up to consider the behaviors of your code, what you should have been testing anyways.
Immutability
Immutability plays a big part in Spec# as well. To some extent, I'll cover more in a Domain Driven Design post, but instead will get some things out of the way here. Eric Lippert, C# team member, has stated that immutable data structures are the way of the future in C# going forward. Spec# can make that move a bit more painless? How you might ask? Well, the ImmutableAttribute lays out that explicitly. Let's do a simple ReadOnlyDictionary in Spec#, taking full advantage of Spec#'s attributes, preconditions and postconditions:
using System;
using System.Collections;
using System.Collections.Generic;
using Microsoft.Contracts;
namespace Microsoft.Samples
{
[Immutable]
public class ReadOnlyDictionary<TKey, TValue> : ICollection<KeyValuePair<TKey!, TValue>> where TKey : class
{
private readonly IDictionary<TKey!, TValue>! dictionary;
public ReadOnlyDictionary(IDictionary<TKey!, TValue>! dictionary)
{
this.dictionary = dictionary;
}
public TValue this[TKey! key]
{
get
requires ContainsKey(key);
{ return dictionary[key]; }
}
[Pure]
public bool ContainsKey(TKey! key)
{
return dictionary.ContainsKey(key);
}
void ICollection<KeyValuePair<TKey!,TValue>>.Add(KeyValuePair<TKey!, TValue> item)
{
throw new NotImplementedException();
}
void ICollection<KeyValuePair<TKey!,TValue>>.Clear()
{
throw new NotImplementedException();
}
[Pure]
public bool Contains(KeyValuePair<TKey!, TValue> item)
{
return dictionary.Contains(item);
}
[Pure]
public void CopyTo(KeyValuePair<TKey!, TValue>[]! array, int arrayIndex)
requires arrayIndex >=0 && arrayIndex < Count;
{
dictionary.CopyTo(array, arrayIndex);
}
[Pure]
public int Count
{
get
ensures result >= 0;
{ return dictionary.Count; }
}
[Pure]
public bool IsReadOnly
{
get
ensures result == true;
{ return true; }
}
[Pure]
bool ICollection<KeyValuePair<TKey!,TValue>>.Remove(KeyValuePair<TKey!, TValue> item)
{
throw new NotImplementedException();
}
[Pure]
public IEnumerator<KeyValuePair<TKey!, TValue>>! GetEnumerator()
{
return dictionary.GetEnumerator();
}
[Pure]
IEnumerator! System.Collections.IEnumerable.GetEnumerator()
{
return dictionary.GetEnumerator();
}
}
}
As you can see, I marked the class itself as immutable. But as well, I removed anything that might change the state of our dictionary, as well as mark things with non-null values. That's a little extra on top, but still very readable. I'll be covering more in the near future as it applies to Domain Driven Design.
Call to Action
So, the call to action is clear, make Spec# a priority to get it in C# going forward. Greg Young has started the campaign, so we need to get it moving!
