Thursday, October 30, 2008 11:35 PM
Enforcing Your Domain Model With Spec#: Part 1: Introduction And The Non-Null Operator
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)
3: return o.ToString(); // NullReferenceException
6: public void Bar()
8: object o = null;
9: string str = Foo(o);
The Spec# way:
1: public string Foo(object! o)
3: return o.ToString();
6: public void BadBar()
8: object o = null;
9: string str = Foo(o); // Spec# warning
12: public void GoodBar()
14: object o = null;
16: if (o != null) // We're ok
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
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
9: get; private set;
12: public int Quantity
14: get; set;
20: public class PurchaseOrder
24: public OrderLineItem AddProduct(IProduct! product, int quantity)
26: // Add product - no need to check for null
32: public class Cart
34: public void Add(IProduct product)
36: if (product != null)
37: PurchaseOrder.AddProduct(product, 1);
39: // Handle null product
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!
Filed under: .NET, Spec#, Domain Driven Design