Spec# To Be Replaced By Code Contracts?

lasseeskildsen — Sun, 16 Nov 2008 23:19:01 GMT

As you might have seen from a previous post I'm pretty excided on Spec# from Microsoft Research, so when my collegue Søren returned from PDC and he told me that Spec# would replaced by Code Contracts I felt kind of disappointed. However, having looked briefly at Code Contracts I must admit that it looks pretty cool. It is especially worth noticing that Code Contract seems to be working well with Pex. How cool would it be to be able to test your domain model with Pex! Because of this, the next articles on Spec# is put on hold, but will eventually continue as either Code Contracts or Spec# posts (actually hoping it's going to be Code Contracts).

I haven't been able to find more on this anywhere, so please do not just take my word for it. However, a couple of team members are both on the Spec# and the Code Contracts team. Feel free to drop a comment if you have more info on this!

Enforcing Your Domain Model With Spec#: Part 1: Introduction And The Non-Null Operator

lasseeskildsen — Thu, 30 Oct 2008 21:35:09 GMT

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; 

    }

  

    public int Quantity

    {

        get; set;

    }

  

    ...

}

  

public class PurchaseOrder

{

    ...

  

    public OrderLineItem AddProduct(IProduct! product, int quantity)

    {

        // Add product - no need to check for null

    }

  

    ...

}

  

public class Cart

{

    public void Add(IProduct product)

    {

        if (product != null)

            PurchaseOrder.AddProduct(product, 1);

        else

            // 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!

Lasse Eskildsen : Domain Driven Design

Spec# To Be Replaced By Code Contracts?

Enforcing Your Domain Model With Spec#: Part 1: Introduction And The Non-Null Operator

So What Is Spec#?

The Non-Null Operator