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

In a previous post, I talked about the essentials of Spec# and where it's going.  After the first post, I talked with Greg Young a little bit about the possibilities and potential of Spec# and Design by Contract.  Greg gave a session on Spec# at DevTeach, so it's great to talk to someone passionate about this technology.  I think it has huge potential to start describing our applications a bit better and moving towards a Domain Driven Design and even Behavior Driven Development.  It gets us away from the simple TDD approaches of checking for null values, preconditions, postconditions and gets you to test at a different level.

Anyhow, today, I'm going to pick up where I left off with Method Contracts and some .NET 3.5 goodness.

Method Contracts

Class methods have both pre and postconditions, which check for errors. Preconditions make sure that the context of your method runs in is valid. It is the job of the caller to establish the precondition, so any precondition violation points to an error in the calling code.  Postconditions are guaranteed by the method to hold at method exit. A postcondition violation points to an error in the method itself.

So, you can see where this leads me to think that there's something here for TDD, BDD and DDD, no?

Preconditions

In Spec#, a method precondition is considered to be part of the signature of a method. The precondition should just give enough information to the caller so that they can call the method with the guarantee that they will not cause an unexpected exception to be thrown. This means that the caller must know statically that the condition is true or can test for the condition dynamically.

To use a precondition, use the requires keyword.  Also, a custom exception can be thrown if the precondition fails by using the otherwise keyword.

Let's look at a code sample from that:

public static int Divide(int value1, int value2)
     requires value2 != 0;
{
     return value1 / value2;
}

And another using the otherwise keyword:

public static int Divide(int x, int y)
     requires value2 != 0 otherwise ArgumentException;
{
     return x / y;
}

The above method doesn't check the y parameter for not being zero, instead depends upon the caller never passing that value. It is enforced by a check in the Spec# compiler emits into the code on the callee side at runtime.  When the static verification is used, the body of the method is verified under the assumption that the precondition holds and will produce an error message for calls in the program state in which it can't be proven that our y parameter isn't zero.

In such an example:

Divide(2, 0); // Error

public static int DoBadStuff(int x)
{
     Divide(2, x); // Error, cannot prove that x is not 0
}

public static int DoGoodStuff(int x)
     requires x != 0;
{
     Divide(2, x); // OK
}

Even the Spec# Visual Studio 2005 plugin has a precondition on the base Console application template as follows:
static void Main(string[] args)
     requires args != null && forall{int i in (0:args.Length); args[i] != null};
{
     ...
}

The above code simply checks for the args string array is not null and no values inside the array are null.  Simple, yet effective!

Postconditions

In Spec#, a method postcondition is also considered to be part of the signature of a method. The postcondition should give enough information to any caller so that they can depend on the state after the call. In essence, it tells you what to expect from the method.

 To use a postcondition, use the ensures keyword.  The result keyword may be used when referring to the result of the operation.  The old keyword can be used when referring the value of the parameter at the beginning of the method.

public static int Subtract(int x, int y)
     requires x > y;
     ensures result > y;
{
     return x - y;
}

.NET 3.5

From my previous post, I noted that in the System.Core.dll, there is a hidden implementation of Spec# in the Microsoft.Contracts namespace.  Remember the Contracts class?  In particular, these methods are useful

Contract
Ensures(bool) - Postcondition
Old<T> - Original parameter values that can be referenced
Requires(bool) - Precondition
Requires(Exception) - Precondition with otherwise statement
Result<T> - The result of the method for the postcondition

In particular, let's look again at the BigInteger class.

internal BigInteger(double value)
{
     Contract.Requires(!double.IsInfinity(value) ? null : ((Exception)new OverflowException()));
     Contract.Requires(!double.IsNaN(value) ? null : ((Exception)new OverflowException()));
     ...
}

As you can see, it's using the preconditons with the otherwise statement in C# goodness.  Pretty cool stuff!

Develop, mentor and inspire!

kick it on DotNetKicks.com Posted on Wednesday, December 12, 2007 3:05 AM .NET , Test Driven Development , ALT.NET , Spec# | Back to top


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

# re: .NET 3.5, Design by contract and Spec# Part 2
Requesting Gravatar...
Okay, I hope these ideas/techniques work. The only area I am non-compliant is the REGULAR exercise.
Left by e cigarette reviews on Nov 16, 2010 5:44 AM

Your comment:
 (will show your gravatar)


Copyright © Matthew Podwysocki | Powered by: GeeksWithBlogs.net