Thursday, October 30, 2008 11:35 PM
lasseeskildsen
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)
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!
Filed under: .NET, Spec#, Domain Driven Design