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.
