Geeks With Blogs
Blog Moved to http://podwysocki.codebetter.com/ Blog Moved to http://podwysocki.codebetter.com/
Updates:
Part7: Spec# Wrapup

On an ongoing coverage of Spec#, I've decided to post some of the actual results of a sample Spec# class and what the results look like in C# and even IL.

Let's get caught up to the previous posts before we continue:
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

By the way, I may have failed to mention that there is a great DotNetRocks broadcast with Rustan Leino, the lead researcher on Spec# which is well worth a listen and can be found here.

Anyhow, let's start with a simple example of a NonNullStringCollection.  I'll be a little lazy and use an ArrayList behind the scenes, but let's look for how you handle the method contracts.  We'll use preconditions and postconditions, non null types and so on.

using System;
using System.Collections;

namespace SpecSharpSample
{
    public class NonNullStringCollection
    {
        private ArrayList! data;
   
        public NonNullStringCollection()
        {
            this.data = new ArrayList();
            base(); // Call this after assigning our non-null fields
        }
       
        public int Add(string! value)
             requires value != null otherwise ArgumentNullException;
             requires !this.IsReadOnly otherwise InvalidOperationException;
             ensures Count > 0;       
        {
            return this.data.Add(value);
        }
       
        public void AddRange(string[]! value)
            requires value != null &&
forall{int i in (0:value.Length); value[i] != null} otherwise ArgumentNullException;
            requires !this.IsReadOnly otherwise InvalidOperationException;
        {
            this.data.AddRange(value);
        }
       
        public void Clear()
            requires !this.IsReadOnly otherwise InvalidOperationException;
            ensures Count == 0;
        {
            this.data.Clear();
        }

        public bool Contains(string! value)
            requires value != null otherwise ArgumentNullException;
        {
            return this.data.Contains(value);
        }
       
        public void CopyTo(string[]! array, int index)
            requires array != null otherwise ArgumentNullException;
            requires index >=0 && index < Count otherwise ArgumentOutOfRangeException;
        {
            this.data.CopyTo(array, index);
        }
       
        public void Insert(int index, string! value)
            requires value != null otherwise ArgumentNullException;
            requires !this.IsReadOnly otherwise InvalidOperationException;
            requires index >=0 && index < Count otherwise ArgumentOutOfRangeException;
        {
            this.data.Insert(index, value);
        }

        public void Remove(string! value)
            requires value != null otherwise ArgumentNullException;
            requires !this.IsReadOnly otherwise InvalidOperationException;
        {
            this.data.Remove(value);
        }

        public void RemoveAt(int index)
            requires index >=0 && index < Count otherwise ArgumentOutOfRangeException;
            ensures Count == old(Count) - 1;
        {
            this.data.RemoveAt(index);
        }
       
        public int Count
        {
            get
                ensures result >= 0;
            {
                return this.data.Count;
            }
        }
       
        public bool IsReadOnly
        {
            get
                ensures result == false;
            {
                return false;
            }
        }
       
        public bool IsSynchronized
        {
            get
                ensures result == false;
            {
                return false;
            }
        }
       
        public string this[int index]
        {
            get
              requires index >=0 && index < Count otherwise ArgumentOutOfRangeException;
              ensures result != null;
            {
                return (string) this.data[index];
            }
            set
              requires index >=0 && index < Count otherwise ArgumentOutOfRangeException;
              requires value != null;
            {
                this.data[index] = value;
            }
        }
    }
}

As you can see, I mixed in a bunch of preconditions, postconditions and assertions.  While you are developing in Spec#, you might notice that the Intellisense for Visual Studio offers something pretty interesting. 

Spec# Intellisense

As you may notice, this displays the method contracts for you thus making your life a little easier to fulfill the contracts.  Pretty cool, huh?

Now, let's take a look at some of the code that gets translated by Reflector into IL.  Let's look at the Add method.  Note the preconditions and postconditions as stated in the above class.  Also, note the usage of the NonNullType as well.  I'll highlight the areas of interest below:

.method public hidebysig instance int32 Add(string modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType) 'value') cil managed
{
    .custom instance void [System.Compiler.Runtime]Microsoft.Contracts.RequiresAttribute::.ctor(string) = { string('::!=(optional([System.Compiler.Runtime]Microsoft.Contracts.NonNullType,string),string){$1,null}') Filename=string('E:\\Work\\SpecSharpSample\\Class1.ssc') StartLine=int32(0x10) StartColumn=int32(0x17) EndLine=int32(0x10) EndColumn=int32(0x24) SourceText=string('value != null') }
    .custom instance void [System.Compiler.Runtime]Microsoft.Contracts.RequiresAttribute::.ctor(string) = { string('::!(bool){this@SpecSharpSample.NonNullStringCollection::get_IsReadOnly{}}') Filename=string('E:\\Work\\SpecSharpSample\\Class1.ssc') StartLine=int32(0x11) StartColumn=int32(0x17) EndLine=int32(0x11) EndColumn=int32(0x27) SourceText=string('!this.IsReadOnly') }
    .custom instance void [System.Compiler.Runtime]Microsoft.Contracts.EnsuresAttribute::.ctor(string) = { string('::>(i32,i32){this@SpecSharpSample.NonNullStringCollection::get_Count{},0}') Filename=string('E:\\Work\\SpecSharpSample\\Class1.ssc') StartLine=int32(0x12) StartColumn=int32(0x16) EndLine=int32(0x12) EndColumn=int32(0x1f) SourceText=string('Count > 0') }
    .maxstack 6
    .locals init (
        [0] class [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException exception,
        [1] int32 return value,
        [2] class [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException SS$Contract Marker,
        [3] int32 SS$Display Return Local)
    L_0000: ldarg.1
    L_0001: ldnull
    L_0002: beq L_000c
    L_0007: br L_0017
    L_000c: ldstr "value"
    L_0011: newobj instance void [mscorlib]System.ArgumentNullException::.ctor(string)
    L_0016: throw
    L_0017: ldarg.1
    L_0018: ldnull
    L_0019: beq L_0023
    L_001e: br L_0029
    L_0023: newobj instance void [mscorlib]System.ArgumentNullException::.ctor()
    L_0028: throw
    L_0029: ldarg.0
    L_002a: call instance bool SpecSharpSample.NonNullStringCollection::get_IsReadOnly()
    L_002f: brtrue L_0039
    L_0034: br L_003f
    L_0039: newobj instance void [mscorlib]System.InvalidOperationException::.ctor()
    L_003e: throw
    L_003f: leave L_0047
    L_0044: stloc.0
    L_0045: rethrow
    L_0047: nop
    L_0048: ldarg.0
    L_0049: ldfld class [mscorlib]System.Collections.ArrayList modopt([System.Compiler.Runtime]Microsoft.Contracts.NonNullType) SpecSharpSample.NonNullStringCollection::data
    L_004e: ldarg.1
    L_004f: callvirt instance int32 [mscorlib]System.Collections.ArrayList::Add(object)
    L_0054: stloc.1
    L_0055: br L_005a
    L_005a: ldarg.0
    L_005b: call instance int32 SpecSharpSample.NonNullStringCollection::get_Count()
    L_0060: ldc.i4.0
    L_0061: ble L_006b
    L_0066: br L_0076
    L_006b: ldstr "Postcondition \'Count > 0\' violated from method \'SpecSharpSample.NonNullStringCollection.Add(optional(Microsoft.Contracts.NonNullType) System.String)\'"
    L_0070: newobj instance void [System.Compiler.Runtime]Microsoft.Contracts.EnsuresException::.ctor(string)
    L_0075: throw
    L_0076: nop
    L_0077: leave L_007f
    L_007c: stloc.2
    L_007d: rethrow
    L_007f: nop
    L_0080: ldloc.1
    L_0081: stloc.3
    L_0082: ldloc.1
    L_0083: ret
    .try L_0000 to L_0044 catch [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException handler L_0044 to L_0047
    .try L_005a to L_007c catch [System.Compiler.Runtime]Microsoft.Contracts.ContractMarkerException handler L_007c to L_007f
}

Now that we looked at the IL, note the exceptions throws and which time.  Now that we have done that, study the code above and check for the assertions, the preconditions and postconditions.  Let's look at a C# version.  Note that it looks very similar to that in the System.Core.dll within the Microsoft.Contracts namespace from some of the classes that we talked about in earlier posts.  Once again, I'll highlight the interesting points below.

[Requires("::!=(optional([System.Compiler.Runtime]Microsoft.Contracts.NonNullType,string),string){$1,null}", Filename=@"E:\Work\SpecSharpSample\Class1.ssc", StartLine=0x10, StartColumn=0x17, EndLine=0x10, EndColumn=0x24, SourceText="value != null"), Requires("::!(bool){this@SpecSharpSample.NonNullStringCollection::get_IsReadOnly{}}", Filename=@"E:\Work\SpecSharpSample\Class1.ssc", StartLine=0x11, StartColumn=0x17, EndLine=0x11, EndColumn=0x27, SourceText="!this.IsReadOnly"), Ensures("::>(i32,i32){this@SpecSharpSample.NonNullStringCollection::get_Count{},0}", Filename=@"E:\Work\SpecSharpSample\Class1.ssc", StartLine=0x12, StartColumn=0x16, EndLine=0x12, EndColumn=0x1f, SourceText="Count > 0")]
public int Add(string modopt(NonNullType) value)
{
    try
    {
        if (value == null)
        {
            throw new ArgumentNullException("value");
        }
        if (value == null)
        {
            throw new ArgumentNullException();
        }
        if (this.IsReadOnly)
        {
            throw new InvalidOperationException();
        }
    }
    catch (ContractMarkerException)
    {
        throw;
    }
    int return value = this.data.Add(value);
    try
    {
        if (this.Count <= 0)
        {
            throw new EnsuresException("Postcondition 'Count > 0' violated from method 'SpecSharpSample.NonNullStringCollection.Add(optional(Microsoft.Contracts.NonNullType) System.String)'");
        }
    }
    catch (ContractMarkerException)
    {
        throw;
    }
    int SS$Display Return Local = return value;
    return return value;
}

Conclusion

As you can see, I'm pretty fascinated with Design by Contract and how it applies to .NET.  I hope that the next version of C# has this as well as other features I'll cover later.  I hope this series was informational and worthwhile as it was for me.  Develop, mentor and inspire!

Please let me know if there is anything I missed or would like to see in this series.

kick it on DotNetKicks.com Posted on Sunday, January 6, 2008 9:58 PM Microsoft , Test Driven Development , ALT.NET , Spec# | Back to top


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

No comments posted yet.
Your comment:
 (will show your gravatar)


Copyright © Matthew Podwysocki | Powered by: GeeksWithBlogs.net