Geeks With Blogs
Blog Moved to http://podwysocki.codebetter.com/ Blog Moved to http://podwysocki.codebetter.com/
Updates:
Part 5: Frame Conditions/Inheritance/Boogie
Part 6: Implementing a non-null string collection
Part7: Spec# Wrapup

Sorry about the delay in getting this post out, but work and the holidays have been busy!  COM and C++ interop have taken a large amount of my time lately for my customer.  I am going to present Spec# to a couple of groups this month, so this should be my motivation to increase the number of posts.

The goal of this series is to better introduce the subject of Spec#.  This product, as wonderful as it is, is not very well documented, so I'm hoping to improve upon that.

For those wanting to follow along with me, the Spec# team has a new version for Visual Studio 2005 which was released on December 27th of this year (version 1.0.11215), which is available here.  Note that not all the quirks have been removed just yet from the VS templates, but it is an improvement.  I'd still like the Solution Explorer to actually work, but oh well!

Anyhow, in my previous posts regarding Spec#, I have discussed some of the general concepts with regard to contracts, invariants, etc.  Let's review each one before we move onto today's topic, because each one builds upon another.

Part 1: Spec# introduction
Part 2: Method Contracts (Preconditions/Postconditions)
Part 3: Invariants

Now that you're caught up to date, let's move onto today's topics:
  • Object Ownership
  • Assertions and Assumptions
Object Ownership

Spec# has another concept we call object ownership.  The idea of this is that every object has at most only one owner, and only this owner may make modifications of this object.  When this is used, references are augmented with a type classification that tells about the ownership releationship between objects. 

There are three types of these references:
  • rep - Representation references say that the object holding the reference is the owner of that referenced object.  The owner can feel free to do anything it wants to with that reference.  The owner may also transfer the ownership rights.  This is the default ownership setting for class fields/properties.

    using Microsoft.Contracts;

    public class CustomerCollection
    {
         [Owned]
         private List<Customer> customers = new List<Customer>();

         public void Add(Customer customer)
           requires customer != null;
         {
              expose(this)
              { // Give up rights to object
                   customers.Add(customer);
              } // Get back rights to object
         }
    }
  • read-only - In Spec#, an object can hold references to objects it doesn't own.  These references are known as read-only references.  These restrict method calls to pure methods and prevent field assignments on them.  Pure methods are methods that do not modify the object state.  These read-only references are marked by using the OwnedAttribute and using the false parameter such as [Owned(false)]

    using Microsoft.Contracts;

    public class CustomerController
    {
         [Owned(false)]
         private ICustomerCollection customerCollection;

         public(ICustomerCollection customerCollection)
         {
              this.customerCollection = customerCollection;
         }
    }
  • peer - If a group of objects have the same owner, they are allowed to modify each other.  These peer objects are marked by the OwnedAttribute and setting the Peer property such as [Owned(Peer=true)].

    public class SteeringWheel
    {
         public void Move(int position) { ... }
    }

    public class Car
    {
         [Owned(Peer=true)]
         private SteeringWheel wheel;

         public void AdjustWheel(int position)
         {
              wheel.Move(position);
         }
    }
Spec# also allows for "unowned" objects which means all references to it are read-only references.  These object have no peers.

Assertions and Assumptions

In the previous posts, we talked about preconditions and postconditions, but now let's talk about assertions and assumptions.  These are inside the method itself.

The Spec# compiler adds support for these assertions through the assert keyword.  Like preconditions and postconditions, these are booleans that are meant to evaluate to true.  The compiler optionally generates code for these assertions and checks them at runtime.  Due to the fact that evaluating these assertions are option, they must not modify anything.

public class Divider
{
     public int DivideByTwo(int x)
       requires x > 0;
     {
          int result = x / 2;
          assert result != 0; // Assumes the result is not zero
          return result;
     }
}

Assumptions, on the other hand are meant for the Boogie static verifier.  I'll talk more about Boogie in the next installment.  Assumptions are facts that the Boogie static verifier will assume is valid.  They are created using the assume keyword.  You must be careful though when specifying these assumptions because it would keep the static verifier from doing its job correctly.  For example, you could be careless in specifying the assumption and it could be wrong, but Boogie won't care and continue with that bad assumption.

public class Divider
{
     public int DivideByTwo(int x)
       requires x > 0;
     {
          int result = x / 2;
          assume result > 0; // Assumes the result is not zero
          ... // Keep going
         return result;
     }
}

Conclusion

So, as you can see, there is a lot to this and I haven't even scratched the surface.  We have yet to cover the other attributes, as poorly documented as they may be, the Boogie static verifier among other things.  Stay tuned!  Develop, mentor and inspire!

kick it on DotNetKicks.com Posted on Friday, December 28, 2007 6:41 PM Microsoft , Test Driven Development , ALT.NET , Spec# | Back to top


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

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


Copyright © Matthew Podwysocki | Powered by: GeeksWithBlogs.net