Blog Moved to http://podwysocki.codebetter.com/

Blog Moved to http://podwysocki.codebetter.com/
posts - 277 , comments - 156 , trackbacks - 27

.NET 3.5, Design by contract and Spec#

Updates:
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
Part7: Spec# Wrapup

As I continue to dig deeper into BDD, TDD and DDD, I've been intrigued by Design by contract and Eiffel.  For a quick introduction for those lazy to visit those links, Design by contract means that designers of software should define precise verifiable interface specifications for software components with abstract data types built upon having business contracts.  Sort of like when a seller and a buyer enter into a contract to sell something, which is mutually beneficial.

So, let's break that into software terms.
  • Impose a precondition which states that the callee must do a certain task for the benefit of itself as well as the caller, who is freed from having to check for other things.
  • Guarantee a certain property or return value on exit as the postcondition
  • Maintain that certain property between calls on the same class.
So, at the end of the day, it comes down to:
  • What does it expect? (The precondition)
  • What does it return (The postcondition)
  • What does it maintain (Class invariant)
The proponents of this design, me included, contend that you should write the assertions first.  So, at the procedural level, we can constrain the following:
  • Acceptable and unacceptable input values and their meanings
  • Return values and their meanings
  • Exception details and their meanings
  • Side effects
  • Preconditions
  • Postconditions
  • Invariants (What it maintains)
Now, enter Spec# into the equation.  What is it?
  • Developed by Microsoft Research
  • Extends C# with specification constructs
  • A compiler that emits runtime checks for the specification constructs
  • A static verifier which proves the run-time checks never fail
  • A plugin to Visual Studio 2003/2005

Spec# in .NET 3.5

Ok, now that you know what it is, why should you care?  As Greg Young notes, sure enough the base of Spec# has come into the .NET 3.5 framework in the System.Core.dll assembly,  Unfortunately, at this time, the classes and attributes are internal, so we cannot make use of them in our code just yet.  But, like the System.Numeric.BigInteger, I expect these classes should be available to us hopefully soon.  As you can see, there are quite a few classes available inside the Microsoft.Contracts namespace:
  • Contract - used for enforcing contracts
  • ContractClassAttribute
  • ImmutableAttribute
  • InvariantAttribute
  • PureAttribute
  • RuntimeContractsAttribute
  • VerifyAttribute
These aren't used all that much just yet, except for the BigInteger class and the new crypto classes.  But if you take a look at the innards of some of these method calls inside Reflector, you'll find it quite interesting.

Take a look at the guts of the Contract class.  You'll find such goodies as this:
  • Assert(bool)
  • AssertOnException
  • AssumeOnReturn
  • Assume(bool)
  • Ensures(bool)
  • Exists(int, int, predicate<int>)
  • Requires(bool)
  • Requires(Exception)
  • Result<T>
  • Throws<E>
  • ThrowsEnsures<E>(bool)
Now let's take a look at the way it's implemented in the BigInteger class in two examples:

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

What the above code means is that the contract states that if the value is either infinity or not a number, then it will throw an OverflowException.  Pretty cool, huh?  Let's look at one more

private static bool IsNegative(byte[] doublebits)
{
     Contract.Requires(doublebits.Length == 8);
     ...
}

Short and to the point, this one says that the contract requires that the length of the byte array must be 8 or else it will fail.  There are plenty more examples if you look around the new libraries based off System.Core.dll.

Spec# Introduction

Now if you visit the Spec# home page, you may be disappointed in the lack of documentation.  Channel 9 comes to the rescue with a Wiki which includes some very limited code samples

Let's walk through the language piece by piece now and go over each topic.  Note that this will be in multiple installments.

Assertions

Assertions are the most basic type in Spec#.  Assertions are checks placed in code for the expected run-time state at a particular execution point. C# has had this in the System.Diagnostics namespace which had boolean expressions that are checked at runtime through the Debug.Assert method.  If evaluation of the boolean expression yielded a false result, then a run-time exception was raised.

Spec# adds an explicit language construct called the assert statement.  The assert statement begins with the keyword assert followed by a boolean expression, and if it returns false, an exception is raised.

C#

public void SaveCustomer(Customer customer)
{
     System.Diagnostics.Debug.Assert(customer != null);
     // Normal code goes here
}

Spec#

public void SaveCustomer(Customer customer)
{
     assert customer != null;
     // Normal code goes here
}

From the above statement, it looks a lot cleaner by abstracting that System.Diagnostics.Debug class out of the picture and makes it seem more correct.  But, let's look at doing this another way with the Non-Null Feature.

Non-Null Feature

In Spec#, we can explicitly detect and warn developers about possible null references/dereferences.  We also have the capability of specifying that a particular parameter cannot be null through the method signature. 

C#

public static void Main(string[] args)
{
     object[] data = null;
     ProcessData(data);
}

public static void ProcessData(object[] data)
{
     foreach(object obj in data) // NullReferenceException
     {
          Console.WriteLine(obj.ToString());
     }
}

Spec#

With Spec#, we will get warned of this possible problem at compile time.

public static void Main(string[] args)
{
     object[] data = null;
     ProcessData(data);
}

public static void ProcessData(object[] data)
{
     foreach(object obj in data) // Warning: possible null reference
     {
          Console.WriteLine(obj.ToString());
     }
}

We can also specify that a null value is not allowed through the use of an exclamation point next to the variable in the method signature.

public static void Main(string[] args)
{
     object[] data = null;
     ProcessData(data); // Error, call not allowed
}

public static void ProcessData(object[]! data)
{
     foreach(object obj in data)  // OK to call
     {
          Console.WriteLine(obj.ToString());
     }
}

Also, if we wish to keep our code C# compliant, we can add them inside a comment block like such as this /*^!^*/

public static void Main(string[] args)
{
     object[] data = null;
     ProcessData(data); // Error, call not allowed
}

public static void ProcessData(object[] /*^!^*/ data)
{
     foreach(object obj in data) // OK
     {
          Console.WriteLine(obj.ToString());
     }
}

Stay tuned for more on this topic in the next part.  There I will cover preconditions, postconditions, invariants, visual studio integration and more.

kick it on DotNetKicks.com

Print | posted on Monday, December 10, 2007 10:53 AM | Filed Under [ Microsoft .NET C# Test Driven Development ALT.NET ]

Feedback

Gravatar

# re: .NET 3.5, Design by contract and Spec#

You seem to be so master and your article just about this good topic supposes to be best. Will you continue your work? I should purchase some phd thesis and just dissertation from you.
1/15/2010 5:08 AM | Gm30Chloe
Gravatar

# re: .NET 3.5, Design by contract and Spec#

This is truly fascinating. Thanks for sharing!
3/28/2010 4:12 AM | Weight Loss Resources
Gravatar

# re: .NET 3.5, Design by contract and Spec#

Thanks for sharing, i have never seen such a great site before
5/28/2010 7:16 AM | thesis writing
Gravatar

# re: .NET 3.5, Design by contract and Spec#

Considerably, the article is actually the best on this laudable topic. I harmonise with your conclusions and will eagerly look forward to your incoming updates. Saying thanks will not just be adequate, for the tremendous lucidity in your writing. I will instantly grab your rss feed to stay informed of any updates. Gratifying work and much success in yourbusiness efforts!
7/31/2010 6:01 PM | jeux pour gagner des cadeaux
Gravatar

# re: .NET 3.5, Design by contract and Spec#

Hello Guru, what entice you to post an article. This article was extremely interesting, especially since I was searching for thoughts on this subject last Thursday.
8/8/2010 9:36 PM | stress management techniques
Gravatar

# # re: .NET 3.5, Design by contract and Spec#

Oh your posts make me very excited! Thank you very much.
1/18/2011 1:35 PM | cv writing service
Gravatar

# re: .NET 3.5, Design by contract and Spec#

eDev Technologies provides requirements definition tool to sufficiently fill the of information lacking in requirements gathering phase.
2/24/2011 12:26 AM | requirements definition
Gravatar

# re: .NET 3.5, Design by contract and Spec#

I am feeling so lucky to read this page, it's wonderful!!
3/23/2011 2:45 AM | true religion jeans
Gravatar

# re: .NET 3.5, Design by contract and Spec#

It is my pleasure to read this page,I look forward to reading more.
3/23/2011 2:46 AM | ray ban sunglasses
Gravatar

# re: .NET 3.5, Design by contract and Spec#

Hello my friend! I want to say that this article is awesome, nice written and include almost all vital infos. I would like to see more posts like this .
3/24/2011 9:38 AM | essay help
Gravatar

# re: .NET 3.5, Design by contract and Spec#

I was looking for anything about design by contract and found your article which was really helpful. You helped me with assertions, thanks
4/2/2011 2:29 PM | LCD Fernseher Test
Gravatar

# re: .NET 3.5, Design by contract and Spec#

This post is very helpful. I would also like to post an informative post and if ever, I will post something about how to cure panic attacks.
4/5/2011 4:45 AM | alliana
Gravatar

# re: .NET 3.5, Design by contract and Spec#

Metroidfor the Wii looks and plays like a souped up Gamecube game.ray ban sunglassesray ban sunglasses
4/6/2011 2:32 AM | ray ban sunglasses
Post A Comment
Title:
Name:
Email:
Comment:
Verification:
 

Powered by: