Contents tagged with DBC

  • Code Contracts - TDD in a DbC World

    Lately, I've been talking about the new feature coming to .NET 4.0, Code Contracts, which is to bring Design by Contract (DbC) idioms to all .NET languages as part of the base class library.  Last week, I attended QCon, where Greg Young, one of my CodeBetter cohorts, gave a talk titled "TDD in a DbC World" in which he talked about that they are not in conflict, but instead are complementary to a test first mentality.  Both improve upon the usage of the other.

  • Your API Fails, Who is at Fault?

    I decided to stay on the Design by Contract side for just a little bit.  Recently, Raymond Chen posted "If you pass invalid parameters, then all bets are off" in which he goes into parameter validation and basic defensive programming.  Many of the conversations had on the blog take me back to my C++ and early Java days of checking for null pointers, buffer lengths, etc.  This brings me back to some recent conversations I've had about how to make it explicit about what I expect.  Typical defensive behavior looks something like this:

    public static void Foreach<T>(this IEnumerable<T> items, Action<T> action)
    {
        if (action == null)
            throw new ArgumentNullException("action");

        foreach (var item in items)
            action(item);
    }

    After all, how many times have you not had any idea what the preconditions are for a given method due to lack of documentation or non-intuitive method naming?  it gets worse when they don't provide much documentation, XML comments or otherwise.  At that point, it's time to break out .NET Reflector and dig deep.  Believe me, I've done it quite a bit lately.

    The Erlang Way

    The Erlang crowd takes an interesting approach to the issue that I've really been intrigued by.  Joe Armstrong calls this approach "Let it crash" in which you only code to the sunny day scenario, and if the call to it does not conform to the spec, just let it crash.  You can read more about that on the Erlang mailing list here.

    Some paragraphs stuck out in my mind.

    Check inputs where they are "untrusted"
        - at a human interface
        - a foreign language program

    What this basically states is the only time you should do such checks is at the bounds when you have possible untrusted input, such as bounds overflows, unexpected nulls and such.  He goes on to say about letting it crash:

    specifications always  say what to  do if everything works  - but never what  to do if the  input conditions are not met - the usual answer is something sensible - but what you're the programmer - In C etc. you  have to write *something* if you detect an error -  in Erlang it's  easy - don't  even bother to write  code that checks for errors - "just let it crash".

    So, what Joe advocates is not checking at all, and if they don't conform to the spec, just let it crash, no need for null checks, etc.  But, how would you recover from such a thing?  Joe goes on to say:

    Then  write a  *independent* process  that observes  the  crashes (a linked process) -  the independent process should try  to correct the error, if it can't correct  the error it should crash (same principle) - each monitor  should try a  simpler error recovery strategy  - until finally the  error is  fixed (this is  the principle behind  the error recovery tree behaviour).

    It's an interesting approach, but proves to a valuable one for parallel processing systems.  As I dig further into more functional programming languages, I'm finding such constructs useful.

    Design by Contract Again and DDD

    Defensive programming is a key part of Design by Contract.  But, in a way it differs.  With defensive programming, the callee is responsible for determining whether the parameters are valid and if not, throws an exception or otherwise handles it.   DbC with the help of the language helps the caller better understand how to cope with the exception if it can.

    Bertrand Meyer wrote a bit about this in the Eiffel documentation here.  But, let's go back to basics. DbC asserts that the contracts (what we expect, what we guarantee, what we maintain) are such a crucial piece of the software, that it's part of the design process.  What that means is that we should write these contract assertions FIRST. 

    What do these contract assertions contain?  It normally contains the following:
    • Acceptable/Unacceptable input values and the related meaning
    • Return values and their meaning
    • Exception conditions and why
    • Preconditions (may be weakened by subclasses)
    • Postconditions (may be strengthened by subclasses)
    • Invariants (may be strengthened by subclasses)

    So, in effect, I'm still doing TDD/BDD, but an important part of this is identifying my preconditions, postconditions and invariants.  These ideas mesh pretty well with my understanding of BDD and we should be testing those behaviors in our specs.  Some people saw in my previous posts that they were afraid I was de-emphasizing TDD/BDD and that couldn't be further from the truth.  I'm just using another tool in the toolkit to express my intent for my classes, methods, etc.  I'll explain further in a bit down below.

    Also, my heavy use of Domain Driven Design patterns help as well.  I mentioned those previously when I talked about Side Effects being Code Smells.  With the combination of intention revealing interfaces which express to the caller what I am intending to do, and my use of assertions not only in the code but also in the documentation as well.  This usually includes using the <exception> XML tag in my code comments.  Something like this is usually pretty effective:

    /// <exception cref="T:System.ArgumentNullException"><paramref name="action"/> is null.</exception>

    If you haven't read Eric's book, I suggest you take my advice and Peter's advice and do so.

    Making It Explicit

    Once again, the use of Spec# to enforce these as part of the method signature to me makes sense.  To be able to put the burden back on the client to conform to the contract or else they cannot continue.  And to have static checking to enforce that is pretty powerful as well. 

    But, what are we testing here?  Remember that DbC and Spec# can ensure your preconditions, your postconditions and your invariants hold, but they cannot determine whether your code is correct and conforms to the specs.  That's why I think that BDD plays a pretty good role with my use of Spec#. 

    DbC and Spec# can also play a role in enforcing things that are harder with BDD, such as enforcing invariants.  BDD does great things by emphasizing behaviors which I'm really on board with.  But, what I mean by being harder is that your invariants may be only private member variables which you are not going to expose to the outside world.  If you are not going to expose them, it makes it harder for your specs to control such behavior.  DbC and Spec# can fill that role.  Let's look at the example of an ArrayList written in Spec#.

    public class ArrayList
    {
        invariant 0 <= _size && _size <= _items.Length;
        invariant forall { int i in (_size : _items.Length); _items[i] == null };  // all unused slots are null

        [NotDelayed]
        public ArrayList (int capacity)
          requires 0 <= capacity otherwise ArgumentOutOfRangeException;
          ensures _size/*Count*/ == 0;
          ensures _items.Length/*Capacity*/ == capacity;
        {
          _items = new object[capacity];
          base();
        }

        public virtual void Clear ()
          ensures Count == 0;
        {
          expose (this) {
            Array.Clear(_items, 0, _size); // Don't need to doc this but we clear the elements so that the gc can reclaim the references.
            assume forall{int i in (0: _size); _items[i] == null};  // postcondition of Array.Clear
            _size = 0;
          }
        }

    // Rest of code omitted

    What I've been able to do is set the inner array to the new capacity, but also ensure that when I do that, my count doesn't go up, but only my capacity.  When I call the Clear method, I need to make sure the inner array is peer consistent by the way of all slots not in the array must be null as well as resetting the size.  We use the expose block to expose to the runtime to have the verifier analyze the code.  By the end of the expose block, we should be peer consistent, else we have issues.  How would we test some of these scenarios in BDD?  Since they are not exposed to the outside world, it's pretty difficult.  What it would be doing is leaving me with black box artifacts that are harder to prove.  Instead, if I were to expose them, it would then break encapsulation which is not necessarily something I want to do.  Instead, Spec# gives me the opportunity to enforce this through the DbC constructs afforded in the language. 

    The Dangers of Checked Exceptions

    But with this, comes a cost of course.  I recently spoke with a colleague about Spec# and the instant thoughts of checked exceptions in Java came to mind.  Earlier in my career, I was a Java guy who had to deal with those who put large try/catch blocks around methods with checked exceptions and were guilty of just catching and swallowing or catching and rethrowing RuntimeExceptions.  Worse yet, I saw this as a way of breaking encapsulation by throwing exceptions that I didn't think the outside world needed to know about.  I was kind of glad that this feature wasn't brought to C# due to the fact I saw rampant abuse for little benefit.  What people forgot about during the early days of Java that exceptions are meant to be exceptional and not control flow.

    How I see Spec# being different is that since we have a static verification tool through the use of Boogie to verify whether those exceptional conditions are valid.  The green squigglies give warnings about possible null values or arguments in ranges, etc.  This gives me further insight into what I can control and what I cannot.  Resharper also has some of those nice features as well, but I've found Boogie to be a bit more helpful with more advanced static verification.

    Conclusion

    Explicit DbC constructs give us a pretty powerful tool in terms of expressing our domain and our behaviors of our components.  Unfortunately, in C# there are no real valuable implementations that enforce DbC constructs to both the caller and the callee.  And hence Spec# is an important project to come out of Microsoft Research.

    Scott Hanselman just posted his interview with the Spec# team on his blog, so if you haven't heard it yet, go ahead and download it now.  It's a great show and it's important that if you find Spec# to be useful, that you press Microsoft to give it to us as a full feature.

    kick it on DotNetKicks.com

  • Command-Query Separation and Immutable Builders

    In one of my previous posts about Command-Query Separation (CQS) and side effecting functions being code smells, it was pointed out to me again about immutable builders.  For the most part, this has been one area of CQS that I've been willing to let break.  I've been following Martin Fowler's advice on method chaining and it has worked quite well.  But, revisiting an item like this never hurts.  Immutability is something you'll see me harping on time and time again now and in the future.  The standard rules I usually do is immutable and side effect free when you can, mutable state where you must.  I like the opt-in mutability of functional languages such as F# which I'll cover at some point in the near future instead of the opt-out mutability of imperative/OO languages such as C#.

    Typical Builders

    The idea of the standard builder is pretty prevalent in most applications we see today with fluent interfaces.  Take for example most Inversion of Control (IoC) containers when registering types and so on:

    UnityContainer container = new UnityContainer();
    container
        .RegisterType<ILogger, DebugLogger>("logger.Debug")
        .RegisterType<ICustomerRepository, CustomerRepository>();

    Let's take a naive medical claims processing system and building up and aggregate root of a claim.  This claim contains such things as the claim information, the lines, the provider, recipient and so on.  This is a brief sample and not meant to be the real thing, but just a quick example.  After all, I'm missing things such as eligibility and so on.

        public class Claim
        {
            public string ClaimId { get; set; }  
            public DateTime ClaimDate { get; set; }
            public List<ClaimLine> ClaimLines { get; set; }
            public Recipient ClaimRecipient { get; set; }
            public Provider ClaimProvider { get; set; }
        }

        public class ClaimLine
        {
            public int ClaimLineId { get; set; }
            public string ClaimCode { get; set; }
            public double Quantity { get; set; }
        }

        public class Recipient
        {
            public string RecipientId { get; set; }
            public string FirstName { get; set; }
            public string LastName { get; set; }
        }

        public class Provider
        {
            public string ProviderId { get; set; }
            public string FirstName { get; set; }
            public string LastName { get; set; }
        }

    Now our standard builders use method chaining as shown below.  As you note, we'll return the instance each and every time. 

    public class ClaimBuilder
    {
        private string claimId;
        private DateTime claimDate;
        private readonly List<ClaimLine> claimLines = new List<ClaimLine>();
        private Provider claimProvider;
        private Recipient claimRecipient;

        public ClaimBuilder() {}

        public ClaimBuilder WithClaimId(string claimId)
        {
            this.claimId = claimId;
            return this;
        }

        public ClaimBuilder WithClaimDate(DateTime claimDate)
        {
            this.claimDate = claimDate;
            return new ClaimBuilder(this);
        }

        public ClaimBuilder WithClaimLine(ClaimLine claimLine)
        {
            claimLines.Add(claimLine);
            return this;
        }

        public ClaimBuilder WithProvider(Provider claimProvider)
        {
            this.claimProvider = claimProvider;
            return this;
        }

        public ClaimBuilder WithRecipient(Recipient claimRecipient)
        {
            this.claimRecipient = claimRecipient;
            return this;
        }

        public Claim Build()
        {
            return new Claim
           {
               ClaimId = claimId,
               ClaimDate = claimDate,
               ClaimLines = claimLines,
               ClaimProvider = claimProvider,
               ClaimRecipient = claimRecipient
           };
        }

        public static implicit operator Claim(ClaimBuilder builder)
        {
            return new Claim
            {
                ClaimId = builder.claimId,
                ClaimDate = builder.claimDate,
                ClaimLines = builder.claimLines,
                ClaimProvider = builder.claimProvider,
                ClaimRecipient = builder.claimRecipient
            };
        }
    }

    What we have above is a violation of the CQS because we're mutating the current instance as well as returning a value.  Remember, that CQS states:

    • Commands - Methods that perform an action or change the state of the system should not return a value.
    • Queries - Return a result and do not change the state of the system (aka side effect free)
    But, we're violating that because we're returning a value as well as mutating the state.  For the most part, that hasn't been a problem.  But what about sharing said builders?  The last thing we'd want to do is have our shared builders mutated by others when we're trying to build up our aggregate roots.

    Immutable Builders or ObjectMother or Cloning?

    When we're looking to reuse our builders, the last thing we'd want to do is allow mutation of the state.  So, if I'm working on the same provider and somehow change his eligibility, then that would be reflected against all using the same built up instance.  That would be bad.  We have a couple options here really.  One would be to follow an ObjectMother approach to build up shared ones and request a new one each time, or the other would be to enforce that we're not returning this each and every time we add something to our builder.  Or perhaps we can take one at a given state and just clone it.  Let's look at each.

    public static class RecipientObjectMother
    {
        public static RecipientBuilder RecipientWithLimitedEligibility()
        {
            RecipientBuilder builder = new ProviderBuilder()
                .WithRecipientId("xx-xxxx-xxx")
                .WithFirstName("Robert")
                .WithLastName("Smith")
                // More built in stuff here for setting up eligibility
     
            return builder;
        }
    }

    This allows me to share my state through pre-built builders and then when I've finalized them, I'll just call the Build method or assign them to the appropriate type.  Or, I could just make them immutable instead and not have to worry about such things.  Let's modify the above example to take a look at that.

    public class ClaimBuilder
    {
        private string claimId;
        private DateTime claimDate;
        private readonly List<ClaimLine> claimLines = new List<ClaimLine>();
        private Provider claimProvider;
        private Recipient claimRecipient;

        public ClaimBuilder() {}

        public ClaimBuilder(ClaimBuilder builder)
        {
            claimId = builder.claimId;
            claimDate = builder.claimDate;
            claimLines.AddRange(builder.claimLines);
            claimProvider = builder.claimProvider;
            claimRecipient = builder.claimRecipient;
        }

        public ClaimBuilder WithClaimId(string claimId)
        {
            ClaimBuilder builder = new ClaimBuilder(this) {claimId = claimId};
            return builder;
        }

        public ClaimBuilder WithClaimDate(DateTime claimDate)
        {
            ClaimBuilder builder = new ClaimBuilder(this) { claimDate = claimDate };
            return builder;
        }

        public ClaimBuilder WithClaimLine(ClaimLine claimLine)
        {
            ClaimBuilder builder = new ClaimBuilder(this);
            builder.claimLines.Add(claimLine);
            return builder;
        }

        public ClaimBuilder WithProvider(Provider claimProvider)
        {
            ClaimBuilder builder = new ClaimBuilder(this) { claimProvider = claimProvider };
            return builder;
        }

        public ClaimBuilder WithRecipient(Recipient claimRecipient)
        {
            ClaimBuilder builder = new ClaimBuilder(this) { claimRecipient = claimRecipient };
            return builder;
        }

        // More code here for building
    }

    So, what we've had to do is provide a copy-constructor to initialize the object in the right state.  And here I thought I could leave those behind since my C++ days.  After each assignment, I then create a new ClaimBuilder and pass in the current instance to initialize the new one, thus copying over the old state.  This then makes my class suitable for sharing.  Side effect free programming is the way to do it if you can.  Of course, realizing that it creates a few objects on the stack as you're initializing your aggregate root, but for testing purposes, I haven't really much cared. 

    Of course I could throw Spec# into the picture once again as enforcing immutability on said builders.  To be able to mark methods as being Pure makes it apparent to both the caller and the callee what the intent of the method is.  Another would be using NDepend as Patrick Smacchia talked about here.

    The other way is just to provide a clone method which would just copy the current object so that you can go ahead and feel free to modify a new copy.  This is a pretty easy approach as well.

    public ClaimBuilder(ClaimBuilder builder)
    {
        claimId = builder.claimId;
        claimDate = builder.claimDate;
        claimLines.AddRange(builder.claimLines);
        claimProvider = builder.claimProvider;
        claimRecipient = builder.claimRecipient;
    }

    public ClaimBuilder Clone()
    {
        return new ClaimBuilder(this);
    }

    Conclusion

    Obeying the CQS is always an admirable thing to do especially when managing side effects.  Not all of the time is it required such as with builders, but if you plan on sharing these builders, it might be a good idea to really think hard about the side effects you are creating.  As we move more towards multi-threaded, multi-machine processing, we need to be aware of our side effecting a bit more.  But, at the end of the day, I'm not entirely convinced that this violates the true intent of CQS since we're not really querying, so I'm not sure how much this is buying me.  What are your thoughts?

    kick it on DotNetKicks.com

  • Side Effecting Functions Are Code Smells Revisited

    After talking with Greg Young for a little this morning, I realized I missed a few points that I think need to be covered as well when it comes to side effecting functions are code smells.  In the previous post, I talked about side effect free functions and Design by Contract (DbC) features in regards to Domain Driven Design.  Of course I had to throw the requisite Spec# plug as well for how it handles DbC features in C#.

    Intention Revealing Interfaces

    Let's step back a little bit form the discussion we had earlier.  Let's talk about good design for a second.  How many times have you seen a method and had no idea what it did or that it went ahead and called 15 other things that you didn't expect?  At that point, most people would take out .NET Reflector (a Godsend BTW) and dig through the code to see the internals.  One of the examples of the violators was the ASP.NET Page lifecycle when I first started learning it.  Init versus Load versus PreLoad wasn't really exact about what happened where, and most people have learned to hate it.

    In the Domain Driven Design world, we have the Intention Revealing Interface.  What this means is that we need to name our classes, methods, properties, events, etc to describe their effect and purpose.  And as well, we should use the ubiquitous language of the domain to name them appropriately.  This allows other team members to be able to infer what that method is doing without having to dig in with such tools as Reflector to see what it is actually doing.  In our public interfaces, abstract classes and so on, we need to specify the rules and the relationships.  To me, this comes back again to DbC.  This allows us to not only specify the name in the ubiquitous language, but the behaviors as well.

    Command-Query Separation (CQS)

    Dr. Bertrand Meyer, the man behind Eiffel and the author of Object-oriented Software Construction, introduced a concept called Command-Query Separation.  It states that we should break our functionality into two categories:

    • Commands - Methods that perform an action or change the state of the system should not return a value.
    • Queries - Return a result and do not change the state of the system (aka side effect free)

    Of course this isn't a 100% rule, but it's still a good one to follow.  Let's look at a simple code example of a good command.  This is simplified of course.  But what we're doing is side effecting the number of items in the cart. 

    public class ShoppingCart
    {
        public void AddItemToCart(Item item)
        {
            // Add item to cart
        }
    }

    Should we use Spec# to do this, we could also check our invariants as well, but also to ensure that the number of items in our cart has increased by 1.

    public class ShoppingCart
    {
        public void AddItemToCart(Item item)
            ensures ItemsInCart == old(ItemsInCart) + 1;
        {
            // Add item to cart
        }
    }

    So, once again, it's very intention revealing at this point that I'm going to side effect the system and add more items to the cart.  Like I said before, it's a simplified example, but it's a very powerful concept.  And then we could talk about queries.  Let's have a simple method on a cost calculation service that takes in a customer and the item and calculates.

    public class CostCalculatorService
    {
        public double CalculateCost(Customer c, Item i)
        {
            double cost = 0.0d;
           
            // Calculate cost
           
            return cost;
        }
    }

    What I'm not going to be doing in this example is modifying the customer, nor the item.  Therefore, if I'm using Spec#, then I could mark this method as being [Pure].  And that's a good thing.

    The one thing that I would hold an exception for is fluent builders.  Martin Fowler lays out an excellent case for them here.  Not only would we be side effecting the system, but we're also returning a value (the builder itself).  So, the rule is not a hard and fast one, but always good to observe.  Let's take a look at a builder which violates this rule.

    public class CustomerBuilder
    {
        private string firstName;

        public static CustomerBuilder New { get { return new CustomerBuilder(); } }
       
        public CustomerBuilder WithFirstName(string firstName)
        {
            this.firstName = firstName;
            return this;
        }

        // More code goes here
    }

    To wrap things up, things are not always fast rules and always come with the "It Depends", but the usual rule is that you can't go wrong with CQS.

    Wrapping It Up

    These rules are quite simple for revealing the true intent of your application while using the domain's ubiquitous language.  As with anything in our field, it always comes with a big fat "It Depends", but applying the rules as much as you can is definitely to your advantage.  These are simple, yet often overlooked scenarios when we design our applications, yet are the fundamentals.

    kick it on DotNetKicks.com

  • Design by Contract Revisited with C# and .NET

    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.

    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
    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.

    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...

    kick it on DotNetKicks.com