In a previous post, I talked about various attempts at frameworks that are trying to do Design By Contract (DBC) in .NET. Many simply just come across as simple validation frameworks without the heart of DBC which is the contract. Where is the contract? Well, dig through my code and find out! It's something that I've been harping on time and time again is that without transparency to the caller and callee of the contract, it's just another validation framework. You'll hear either myself or Greg Young on that, I'm sure.
The only approach that has worked so far has been Spec# in the .NET world. Unfortunately, still a research product, isn't available for us to use commercially. So, until that time in which it is thoroughly weaved into the .NET framework as a whole outside of the internals of System.Core.dll, we have to look at alternatives.
EiffelBefore we look at another framework, I just want to walk you through a sample of the original DBC language, Eiffel. This gives you an idea what I'm talking about.
my_list.do_all (agent (s: STRING)
require
not_void: s /= Void
do
s.append_character (',')
ensure
appended: s.count = old s.count + 1
end)
As you can see, it's clearly stated as part of the language what the requirements are, and what its return will be. That's the really slick part about it that we don't have unless we go to
Eiffel.NET, but it's not using the latest and greatest .NET APIs, so it's pretty much a nonstarter. So, let's look at yet another framework.
LinFu DesignByContractPhilip Laureano, who has done a lot with LinFu including Aspect Oriented Programming (AOP) among other things has taken a stab at DBC for all .NET languages and not just C# which Spec# has done. He posted the LinFu.DesignByContract2 article on
CodeProject that is well worth checking out.
Earlier, he posted one about the LinFu framework on
CodeProject as well which includes the following:
- A simple IoC container
- Design by Contract framework
- Dynamic Proxy
- Reflection (Mixins, Duck Typing and Multiple Dispatch)
- Delegates with lambdas for universal event handling
But, let's get back to the DBC part, you'll remember the basic tenets of the philosophy:
- What do we expect?
- What do we return?
- What do we maintain?
We also throw in a few Eiffel constructs in terms of inheritance which are also quite important. And they are:
- The precondition may only be weakened by inheritance
- The postcondition can only be strengthened by inheritance
Well, enough about the basics, let's look at the framework itself. Let's first look at a simple sample I whipped up:
public class StringCollection{
private int count;
string[] strings =
new string[5];
[
EnsureCountIncremented]
public virtual void Add([NotNull] string value)
{
// NotNull doing // Debug.Assert(!string.IsNullOrEmpty(value)); // Add value and redefine // EnsureCountIncremened // Debug.Assert(count == count + 1); }
}
So, what you see here is that I put a postcondition making sure that the count is incremented by one as I'm adding a string to my array. Also, I have the precondition that my string value is not null. But, how does that work?
In order to do that we need to implement a few interfaces. Let's look at the one for preconditions.
public interface IMethodContract{
IList<IPrecondition> Preconditions {
get; }
IList<
IPostcondition> Postconditions {
get; }
}
public interface IPrecondition :
IMethodContractCheck{
bool Check(
object target,
InvocationInfo info);
void ShowError(
TextWriter output,
object target,
InvocationInfo info);
}
Ok, so now, I need to implement that somehow for my custom attribute. That would look similar to this:
public sealed class NotNullAttribute :
Attribute,
IPrecondition{
public bool Check(
object target,
InvocationInfo info)
{
string value = target
as string;
if(!
string.IsNullOrEmpty(
value))
return true;
}
public void ShowError(
TextWriter output,
object target,
InvocationInfo info)
{
output.WriteLine(
"string value cannot be null or blank");
}
public bool AppliesTo(
object target,
InvocationInfo info)
{
return target
is string;
}
public void Catch(
Exception ex)
{
}
}
So, it's pretty interesting and clever how this is being done. But still without the static checking of Boogie and so on, it still falls well short of real DBC.
For those interested in postconditions and invariants, those are also supported through the interfaces as shown below:
public interface IPostcondition : IMethodContractCheck
{
void BeforeMethodCall(object target, InvocationInfo info);
bool Check(object target, InvocationInfo info, object returnValue);
void ShowError(TextWriter output, object target, InvocationInfo info,
object returnValue);
}
public interface IInvariant : IContractCheck
{
bool Check(object target, InvocationInfo info, InvariantState callState);
void ShowError(TextWriter output, object target, InvocationInfo info,
InvariantState callState);
}
So, as I said, quite interesting and clever the way of handling the DBC concepts through interfaces. The libraries were also written to support the Eiffel constructs of inheritance. So, very well written I must admit.
ConclusionI just began to scratch the surface with what you can do with this framework and it's very well written. But, still at the end of the day, it's not statically checked through a Boogie and a theorem prover to ensure the contracts hold. That's the crucial part missing in this equation. I'm sure more will come to mind on the subject. Until next time...
