I'm a huge fan of Domain Driven Design (DDD) (links here, here and here) and this post is the first in many, all about enforcing your domain model using Spec#.

So What Is Spec#?

Spec# is a super set of C# 2.0 (no, unfortunately not 3.0 yet). This means that Spec# has all the features as C#, and all the Spec# stuff on top of that.

Spec# is about specifying, and because the guys at Microsoft probably explains it better than I do, I have stolen copied this from the Spec# web site:

• The Spec# programming language.  Spec# is an extension of the object-oriented language C#.  It extends the type system to include non-null types and checked exceptions.  It provides method contracts in the form of pre- and postconditions as well as object invariants.
• The Spec# compiler.  Integrated into the Microsoft Visual Studio development environment for the .NET platform, the compiler statically enforces non-null types, emits run-time checks for method contracts and invariants, and records the contracts as metadata for consumption by downstream tools.
• The Spec# static program verifier.  This component (codenamed Boogie) generates logical verification conditions from a Spec# program.  Internally, it uses an automatic theorem prover that analyzes the verification conditions to prove the correctness of the program or find errors in it.

This first post explains the non-null operator, so let's get to it.

The Non-Null Operator

The non-null operator is probably the most simple operator in Spec#, yet I find it very effecient to express e.g. value objects or aggregates in the domain.

The non-null operator is in a way the opposite as the nullable operator in C#, which allows value types to be nullable. The non-null operator allows you to specify reference types as being non-nullable by using an exclamation mark (!).

The C# way:

   1: public string Foo(object o)

   2: {

   3:     return o.ToString(); // NullReferenceException

   4: }

   5:  

   6: public void Bar()

   7: {

   8:     object o = null;

   9:     string str = Foo(o);

  10: }

The Spec# way:

   1: public string Foo(object! o)

   2: {

   3:     return o.ToString();

   4: }

   5:  

   6: public void BadBar()

   7: {

   8:     object o = null;

   9:     string str = Foo(o); // Spec# warning

  10: }

  11:  

  12: public void GoodBar()

  13: {

  14:     object o = null;

  15:  

  16:     if (o != null) // We're ok

  17:         Foo(o); 

  18: }

If o was initialized to something else than null in GoodBar() the Spec# compiler would be happy too.

In a domain example an implementation could be something like this:

   1: public class OrderLineItem

   2: {

   3:     ...

   4:  

   5:     // We're making the product property non-nullable as an order line item without a product

   6:     // does not make much sense, it would just be a quantity of nothing.

   7:     public IProduct! Product

   8:     {

   9:         get; private set; 

  10:     }

  11:  

  12:     public int Quantity

  13:     {

  14:         get; set;

  15:     }

  16:  

  17:     ...

  18: }

  19:  

  20: public class PurchaseOrder

  21: {

  22:     ...

  23:  

  24:     public OrderLineItem AddProduct(IProduct! product, int quantity)

  25:     {

  26:         // Add product - no need to check for null

  27:     }

  28:  

  29:     ...

  30: }

  31:  

  32: public class Cart

  33: {

  34:     public void Add(IProduct product)

  35:     {

  36:         if (product != null)

  37:             PurchaseOrder.AddProduct(product, 1);

  38:         else

  39:             // Handle null product        

  40:     }

  41: }

In the example above, the caller of PurchaseOrder.AddProduct is forced to check for null before calling the method. This really encapsulates clean business logic in the PurchaseOrder and OrderLineItem classes. In C# you would create a guard clause at the top of the AddProduct method, but in order for a developer to know about this, he has to read the implementation of the method. By using Spec# the developer is made aware of this when calling the method.

Please feel free the leave a comment or contact me of you have any questions or comments!

Part 2 is all about preconditions... Coming up!