Geeks With Blogs
Blog Moved to http://podwysocki.codebetter.com/ Blog Moved to http://podwysocki.codebetter.com/
Update:  the following updates:
Part 6: Implementing a non-null string collection
Part7: Spec# Wrapup

Well, I thought I'd find some distraction from watching my Hokies losing to Kansas right now 14-17.  Boo!  Oh well, let's get back to our coverage of Spec#.  Let's get caught up to where we are so far.  Review each of these before we continue.

Part 1: Spec# introduction
Part 2: Method Contracts (Preconditions/Postconditions)
Part 3: Invariants
Part 4: Object Ownership/Assertions & Assumptions

So, once again, now that we're up to date, let's move onto two of the more fun topics.  Today, we're going to cover the following:
  • Frame Conditions
  • Inheritance
  • Boogie
Frame Conditions

Spec# introduces a concept called frame conditions.  This concept allows you to restrict which pieces of the state that a particular method is allowed to modify.  This is specified by using the modifies keyword.  Let's walk through a basic example

public class Adder
{
    private int sum;
    private int unchangedValue;
   
    public int Add(int x) modifies sum;
    {
        sum += x;
        return sum;
    }
}

In the above example, I created a method called Add which is allowed to modify the state of sum, but changes to any other variables such as unchangedValue is not allowed.  The state of unchangedValue must remain the same from entry to exit.

Interesting concept, but how likely is it that you want to expose your member variables as part of your method contract?  Instead, Spec# allows for the concept of wildcards.  This allows you to modify the fields of the object through a simple statement.  The documentation states that the ^ can be used to denote a wildcard but I cannot get it to work.  The below code should work according to the original spec:

public class Adder
{
    private int sum;
   
    public int Add(int x) modifies this^Adder;
    {
        sum += x;
        return sum;
    }
}

What the wildcard allows is that I can modify all fields within my Adder class.  What's interesting about the wildcards is that they don't extend to aggregate objects.  Take for an example, StringCollection.  If I put a modifies wildcard on the Add method, I can modify the count and the reference to the string array, but I cannot modify the array elements.

These frame conditions only serve as documentation as they are not enforced at runtime.  Instead, they are used by, yes, there's that word again, Boogie.  There are two reasons for this not being checked at runtime.  First is performance since the preconditions and postconditions must be checked in the heap, and second is that if you are making a transition to C#, it makes it easier not to have these as run time errors.

Inheritance of Specifications

In Spec#, your method's contract is inherited by the method's overrides.  The run-time checks evoked by the method contract are also inherited as well.  This helps make documentation more readable than say the MSDN where we have to read the documentation about the preconditions for a particular method.

Additional postconditions can be added to your class through the use of the ensures keyword.  The override can add exception causing postconditions only for those exceptions that are already covered by the throws set, meaning that you've already declared your method throws them. You are not allowed to give any additional frame conditions, instead it's best by adding a postcondition. Changes to the preconditions are also not allowed, because the callers expect the specification at the static resolution of the method to agree with the dynamic checking.

Below is an example of adding an additional postcondition:

public class Foo
{
    public int Index;
   
    public virtual void Increment() ensures Index > 0;
    {
        Index++;
    }
}

public class Bar : Foo
{
    public override void Increment() ensures Index == old(Index) + 1;
    {
        Index++;
    }
}

Interfaces, much like classes can also have methods with specifications.  With these interfaces, you can have multiple inheritance.  Spec# combines these inherited specifications, much like the postconditions.  For the Exception throwing specifications, they must have the same throws declared or else it won't work.  Like with class inheritance, the preconditions are not combined unless they are the same as well.

Boogie

I know it took me a while to get to Boogie, but it's one of the most important pieces of Spec#.  Boogie is a static verifier that attempts to statistically prove that a program functions correctly by translating the given Spec# program into it's own intermediate language called BoogiePL.  The BoogiePL is a simple language consisting of methods with four kinds of statements, assignments, asserts, assumes and method calls.  The BoogiePL program goes through several transformations before it is fed to a theorem prover.  Microsoft is using their own internal verifier now as part of boogie, called Z3.

What's really nice is that it checks whether the contract is fulfilled.  If not, developers are warned at development time that they're not working conform the contract.   To use Boogie, simply go to the Spec# command prompt as installed when you installed Spec#.  Simply type Boogie and the full path to your assembly.  From there, the magic happens.  Here is a simple output:

E:\Work\Project1\bin\debug>boogie project1.exe
Spec# Program Verifier Version 0.88, Copyright (c) 2003-2007, Microsoft.
Program.ssc(34,4): Error: Assertion might not hold: result > 0
Program.ssc(44,4): Error: Possible null dereference
Program.ssc(95,13): Error: Call of string.Replace(string! oldValue, string newVa
lue), unsatisfied precondition: oldValue.Length > 0
Program.ssc(78,20): Related information:     (trace position)

Spec# Program Verifier finished with 5 verified, 3 errors

Pretty cool, huh?  These errors of course can be fixed with our preconditions, postconditions and invariants.

Conclusion

I think I have one more post in me about diving deep into Spec#.  it's a wonderful concept that I hope makes its way into either the BCL for .NET 4.0, or just even to C# vNext.  One can dream....

I believe firmly that Design by Contract with Spec# has an opportunity to change the way Test Driven Development and even Behavior Driven Development is done due to specifying the contract inside the class and method signature itself.  This also greatly improves documentation about the expected behaviors of your code to a whole new level.  Imagine not having to dig through the MSDN to find the expected behaviors of the code, and instead, have it in the method signature itself!

kick it on DotNetKicks.com Posted on Friday, January 4, 2008 1:12 AM Spec# | Back to top


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

# re: .NET 3.5, Design by contract and Spec# Part 5
Requesting Gravatar...
Hey,

Its Nice one...


Left by Nisheeth on Feb 11, 2008 2:11 AM

Your comment:
 (will show your gravatar)


Copyright © Matthew Podwysocki | Powered by: GeeksWithBlogs.net