Geeks With Blogs
Blog Moved to http://podwysocki.codebetter.com/ Blog Moved to http://podwysocki.codebetter.com/
Update: Adding Visual Studio Integration discussion
Update: Stay tuned for additional posts in this series as things permit

Well, this is my last post in the series to wrap things up.  This will be updated as things come to mind, as they always do in a series like this.  There may have been unclear things that I will attempt to explain a little further, plus clarify and explore new things.

Let's get caught up from the series:
Part 1: Spec# introduction
Part 2: Method Contracts (Preconditions/Postconditions)
Part 3: Invariants
Part 4: Object Ownership/Assertions & Assumptions
Part 5: Frame Conditions/Inheritance/Boogie
Part 6: Implementing a non-null string collection in Spec#

Now let's go over some topics I may have missed earlier:
  • Constructor behavior
  • Pure methods
  • Immutables
  • Visual Studio Integration with C#
Constructor Behavior

When using non-null types in your Spec# code, you need to be careful about when your object is initialized.  In .NET, the order of the calling of constructors is non-deterministic, meaning that the base constructor may be called before the super class's.  In Spec#, if you have a non-null field declared, you must initialize it, so therefore you need to control the order in which the constructors are called.  Fortunately, Spec# gives you that capability, and allows you to call the base constructor at any time during the constructor of your superclass through the use of the base keyword.  Below is an example of that:

public class NonNullStringCollection
{
     private List<string!>! strings;

     public NonNullStringCollection()
     {
          strings = new List<string!>();
          Debug.WriteLine("Before base constructor");
          base(); // Must call this after initializing all non-null fields
          Debug.WriteLine("After base constructor");
     }
}

So, unlike C# and others, we have the ability to control the flow of our constructors.  By this, it is pretty powerful as we need to do this.  How does it look like in IL where I'll highlight where it verifies the call of the constructor
.method public hidebysig specialname rtspecialname instance void .ctor() cil managed
{
    .maxstack 8
    L_0000: ldarg.0
    L_0001: newobj instance void [mscorlib]System.Collections.Generic.List`1<string modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType)>::.ctor()
    L_0006: stfld class [mscorlib]System.Collections.Generic.List`1<string modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType)> modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType) SpecSharpSample.NonNullStringCollection::data
    L_000b: ldstr "Before base constructor"
    L_0010: call void [System]System.Diagnostics.Debug::WriteLine(string)
    L_0015: ldarg.0
    L_0016: call instance void [mscorlib]System.Object::.ctor()
    L_001b: ldstr "After base constructor"
    L_0020: call void [System]System.Diagnostics.Debug::WriteLine(string)
    L_0025: ret
}

If you look at the C# version through Reflector, you'll notice no difference whatsoever:

public NonNullStringCollection()
{
    this.data = new List<string modopt(NonNullType)>();
    Debug.WriteLine("Before base constructor");
    Debug.WriteLine("After base constructor");
}

Pure Methods

If you want to call a method in a specification, then the method you call must be pure, which means it has no effect on the state of objects allocated at the time the method is called.  In order for a method to be considered pure, it must be marked with the PureAttribute, ConfinedAttribute or StateIndependentAttribute in the Microsoft.Contracts namespace.  In order to do this, it's rather easy:

[Pure]
public void DoesNotModifyState() { ... }

All three of the above attributes mark the method as pure.  It also declares what the method may read, so let's look at that below:
  • PureAttribute - this method may read anything
  • ConfinedAttribute - this method can only read the state of the receiver object and its representation objects
  • StateIndependentAttribtue - this method does not read any mutable part of the heap.
Over time, it's the plan of the team to migrate to just a simple PureAttribute and I'm not sure as of this writing if that is done.  The default read permission is set to the ConfinedAttribute, so until the name change is complete, it's best to use that one.

Immutables

Some objects in the .NET framework will remain "peer consistent" forever once their constructor has finished.  Recall back to the ownership and invariants discussion for that definition.  If a type is marked with the ImmutableAttribute, then the fields and such are not allowed to be modified once it has left the constructor.  To think about these, think of such objects as DateTime, Guid and other value objects, by the fact that you cannot modify them once they have been created.

[Immutable]
public classCoordinate
{
     public Coordinate()
     {
          this.longitude = LongitudeMinValue;
          this.latitude = LatitudeMaxValue;
          base();
     }

     public Coordinate(double latitude, double longitude)
     {
          this.longitude = longitude;
          this.latitude = latitude;
          base();
     }

     public Coordinate Add(double latitude, double longitude)
     {
          return new Coordinate(this.latitude + latitude, longitude + this.longitude);
     }
}

As you can note, I'm not changing this after I've finished constructing them.  I don't mean Value Objects in the DDD sense of the word, although it could possibly apply here as well when it comes to Entities versus Value Objects.  Anyhow, by default, these value objects are peer consistent.  The String class is immutable, so your program can always invoke methods on strings because since it is always immutable, it will always be peer consistent.

In order to make your own objects immutable, you need to make sure it has no peers.  The static verifier, Boogie, checks to make sure no expose operations (expose keyword) is applied in the class as well.  Fields using the PeerAttribute are not allowed in immutable classes.  Also, there is no need to own an immutable object, since the reason for owning an object is to keep it peer consistent, and by default, immutable objects are peer consistent.

There are three restrictions you must note when using an immutable object.
  • A Constructor of an immutable class must end by calling its base constructor.
  • Can only be declared if the base class is also immutable
  • A class or interface that derives from an immutable type must also be declared immutable.
Let's wrap this up with pure methods.  An immutable class can only invoke pure methods on its fields due to the state of the object not being allowed to change.

Visual Studio Integration with C#

When you install Spec# for Visual Studio 2005, by default it will install the project templates for Spec#, which includes the standard stuff plus a few extras including:
  • Class Library
  • Windows Application
  • Console Application
  • Sample Projects
    • ArrayList
    • Bag
    • Subclass with Invariant
    • Use Mscorlib contracts
Now when you choose to use the Spec# templates, you give up a lot of the C# features that you have come to love.  This also hurts especially when using a tool such as Resharper to make me a productive developer.  You also give up auto-indentation as well, so if you want it, you do it yourself!

But, on the positive side of things, you get the feedback from the static verifier to give you the red and green squigglies that display not only syntax errors, but also theorem prover errors coming from Boogie.  How cool is that?  Also, as I mentioned in a previous post, you get Intellisense to display the contracts of other classes as you highlight them.

But, say for instance, you still want the rich environment of C# to do Spec#.  Well, you can do that, too.  In my first post in the series, I alluded to the fact that you could do Spec# in C# but to comment it out so that C# doesn't detect it, but Spec# will.

To make a non-liar out of me, create a new C# project, and right click on the project and go to properties and you should see this following screen:

C# with Spec# Contracts

This screen allows you to do compile time checks on your code as you build it.  First, the project will build in C#, and then hand it off to Spec# for your post-compilation.  It's probably a similar process to what the BCL team did when they incorporated the Microsoft.Contracts namespace into System.Core.dll.

To use these Spec# contracts in your C# code, it's as simple as commenting out your contracts with this:
/*^ Do Spec# thing here; ^*/

Below is a quick example of this:

public class NonNullStringCollection
{
    private List<string/*^!^*/>/*^!^*/ strings;

    public NonNullStringCollection()
    {
        strings = new List<string/*^!^*/>();
        /*^base();^*/
    }

    public void Add(string/*^!^*/ value)
        /*^requires value != null;^*/
        /*^ensures Count == old(Count) + 1;^*/
    {
        strings.Add(value);
    }

    public int Count
    {
        get
            /*^ensures result >= 0; ^*/
        {
            return strings.Count;
        }
    }
}

Let's look at the constructor to make sure our base constructor gets called last:

    .method public hidebysig specialname rtspecialname instance void .ctor() cil managed
    {
        .maxstack 8
        L_0000: ldarg.0
        L_0001: newobj instance void [mscorlib]System.Collections.Generic.List`1<string modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType)>::.ctor()
        L_0006: stfld class [mscorlib]System.Collections.Generic.List`1<string modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType)> modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType) NonNullTypes.NonNullStringCollection::strings
        L_000b: ldarg.0
        L_000c: call instance void [mscorlib]System.Object::.ctor()
        L_0011: ret
    }

If you try compiling without marking base(); in the constructor, you might notice it right at the top of the method call.  Also, let's take a look at the resulting C# created for the Add Method:

[Requires("::!=(optional([System.Compiler.Runtime]Microsoft.Contracts.NonNullType,string),string){$1,null}", Filename=@"E:\Work\NonNullTypes\NonNullStringCollection.cs", StartLine=0x12, StartColumn=0x19, EndLine=0x12, EndColumn=0x26, SourceText="value != null"), Ensures(@"::==(i32,i32){this@NonNullTypes.NonNullStringCollection::get_Count{},::+(i32,i32){\old(this@NonNullTypes.NonNullStringCollection::get_Count{}),1}}", Filename=@"E:\Work\NonNullTypes\NonNullStringCollection.cs", StartLine=0x13, StartColumn=0x18, EndLine=0x13, EndColumn=0x2f, SourceText="Count == old(Count) + 1")]
public void Add(string modopt(NonNullType) value)
{
    int old(Count);
    try
    {
        if (value == null)
        {
            throw new ArgumentNullException("value");
        }
        if (value == null)
        {
            throw new RequiresException("Precondition 'value != null' violated from method 'NonNullTypes.NonNullStringCollection.Add(optional(Microsoft.Contracts.NonNullType) System.String)'");
        }
        old(Count) = this.Count;
    }
    catch (ContractMarkerException)
    {
        throw;
    }
    this.strings.Add(value);
    try
    {
        if (this.Count != (old(Count) + 1))
        {
            throw new EnsuresException("Postcondition 'Count == old(Count) + 1' violated from method 'NonNullTypes.NonNullStringCollection.Add(optional(Microsoft.Contracts.NonNullType) System.String)'");
        }
    }
    catch (ContractMarkerException)
    {
        throw;
    }
}

Conclusion

So, as you can note, there are plenty more opportunities to dig deeper and I hope you all get the bug to do so.  If I missed anything, let me know!  I would love to use such a thing in production, but it's not designed for such right now.  Also, the licensing states that it's for academic uses only at this point.  But, who knows what the future holds for this.  Design, mentor and inspire!

kick it on DotNetKicks.com Posted on Monday, January 7, 2008 11:07 PM Test Driven Development , ALT.NET , Domain Driven Design , Spec# | Back to top


Comments on this post: .NET 3.5, Design by contract and Spec# Wrapup

# Very nice overview
Requesting Gravatar...
Thank you for these nice articles about Spec#.

They have helped greatly me in understanding Spec# and they point out
changes which have occurred since the overview paper of Spec# was written.
Left by Jóhann Haukur Gunnarsson on Feb 18, 2008 7:01 PM

# re: .NET 3.5, Design by contract and Spec# Wrapup
Requesting Gravatar...
Jóhann,

Thanks for the comments. If you felt I missed anything, please let me know.

Matt
Left by Matthew Podwysocki on Feb 18, 2008 7:53 PM

# re: .NET 3.5, Design by contract and Spec# Wrapup
Requesting Gravatar...
Great posts. I'm interested to know more about the PeerAttribute though, is it important?
Left by Colin Jack on Jun 07, 2008 5:07 PM

# Very promising features
Requesting Gravatar...
Thanks for shedding light on this. These are very promising features, although I am afraid they are not going to make it into the next C# 4.0. I 've been watching this chat (http://channel9.msdn.com/posts/Charles/C-40-Meet-the-Design-Team/) with Anders Hejlsberg and others, and it seems like that.

Besides I cannot make VS 2008 to build a project in C#, "and then hand it off to Spec# for your post-compilation." Could you elaborate more on this?
Left by Vicente Almagro on Sep 19, 2008 3:55 AM

Your comment:
 (will show your gravatar)


Copyright © Matthew Podwysocki | Powered by: GeeksWithBlogs.net