Design by Contract Revisited with C# and .NET
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.
Eiffel
Before 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 DesignByContract
Philip 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
- What do we expect?
- What do we return?
- What do we maintain?
- The precondition may only be weakened by inheritance
- The postcondition can only be strengthened by inheritance
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.
Conclusion
I 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...