Spec# - First Impressions

I finally got around to looking properly at Spec#, previously all I've been going on was blogs and podcasts, and I'm very impressed.

Although there are other good resources out there I decided to write about the features I enjoyed using, and obviously if you want to try Spec# yourself you can get it at the Spec# Site.

Non-Nullable Reference Types

If you look at many of my protected or public methods then you'll find code that look out for nulls. Its not particularly interesting code so writing it and testing it is bad enough but for it to be visible to the users of your code you really also need to document it (unless the tests are enough).

Anyway there is little doubt that using ! to indicate that null is not allowed is a far more attractive option:

public void Transfer(Account! source, Account! destination, doubletransfer, IAuthorizationService! authorizationService)

If I then try to pass in null then I do get a warning telling me that "Null cannot be used where a non-null value is expected.", very nice.

Preconditions

I might want to specify some preconditions explicitly to help the caller know what is expected of them:

public TransferDescription! Transfer(Account! source, Account! destination, double amountToTransfer, IAuthorizationService! authorizationService)
requires source != destination;
requires amountToTransfer > 0;

If I now try and call my service passing in the same Account for source and destination then I get a Microsoft.Contracts.RequiresException which is useful.

This feature alone would be great for someone like me, not least as it makes it easy for callers to find about these preconditions:

PostConditions

Postconditions help me describe the promises my member makes to callers. For example here is how I've specified that my method returns a non-null object that contains the amount of the transfer:

public TransferDescription! Transfer(Account! source, Account! destination, double amountToTransfer, IAuthorizationService! authorizationService)
       ensures result.Amount == amountToTransfer;

If the returned object does not have an Amount equal to amountToTransfer then I get a Microsoft.Contracts.EnsuresException.

Invariants

Specifying that some set of conditions "always" holds true can be useful, for example lets say I want my accounts to stay in credit:

 public class Account
{
    private double _balance;
    invariant _balance >= 0;

The result of breaking one of these invariants at run-time is an Microsoft.Contracts.ObjectInvariantException. There is also a way of temporarily breaking invariants within the type, see the expose keyword.

Finding Out More

Google doesn't turn up much until you realize that instead of Spec# you need to search for something like "specsharp". Still there isn't that much out there and in general the documentation regarding Spec# is pretty patchy but there are some decent resources:

1. Making Spec# a Priority and .NET 3.5, Design by contract and Spec#
2. Expert to Expert: Contract Oriented Programming and Spec# - Excellent screen cast showing what Spec# is all about. Hate the talk about "bangs" though :)
3. Spec# Site
4. Declare Your Love

I certainly thought Spec# was worth a few hours of play, I did only scratch the surface but I definitely hope these features are brought into C# sooner rather than later.

Share This - Digg It • Save to del.icio.us • Stumble It! • Kick It • DZone