Contracts as a part of the type system? (No Interface Without Contract – Part 7)

Contracts? What are Contracts? And why are they reputed to be concerned with the type system? Aren’t they just injected into the executable? Is there maybe “more” behind them? And how should they really be used? Read this post for clarification.

Looking back

There have been ? parts of the series “No interface Without Contract?” now. It’s not that I told you everything about Microsoft Code Contracts yet and there is nothing more to introduce. In fact this will not be the last part, but there will follow about three.

If you look at the previous parts, you will notice that they are quite distanced: All their content stands – less or more detailed – in the Code Contract’s manual. Thus, you may have noticed that I did not really go “deeper” by talking about my experience using them.

What are Code Contracts?

The reason for that is simple: I did not really think about one question: What are Code Contracts?

Saying “think” I do not mean that I did not make any thoughts about it. I always knew an answer, but a simple one: Code Contracts can be used in order to formulate pre- and postconditions. During this series, I also explained what pre- and postconditions are; in short: Conditions that should be hold when entering respectively exiting a method.

These thoughts and ideas, however, are quite superficial. They are more definitions or explanations and do not really hit the essential aspects of Code Contracts: In which way should I really use them?

Even if it sounds some way “theatrically”: I now feel ready to answer this question.

Strongly typed languages

Yes – you did not misread this heading: I am going to talk about languages having a strong type system.

“Strongly typed” – you definitely know already – means that the compiler performs some basic checks on how you have to call your methods and how to treat the objects in your application.

The compiler takes care that you do not pass a car instead of a cat and do not multiplicity two persons. And there are good reasons for a behavior like that: Although I do not want to open a discussion about duck typing (the opposite of strong typing) and its advantages / disadvantages, one thing you surely will agree: There are many situations in which it does not make any sense to pass an specific type of object to a method: You do not want to spray your cat – so a method performing this job somehow has to validate that it is no cat it gets.

It would be great to have someone controlling this process: Something like a “no entry for cats” sign at the door of your repair shop (and someone who hinders entering every cat ignoring it).

However, there are also cases in which you would also like your repair shop to spray motorcycles without opening a new branch.

We can formulate one perception: You need some freedom when using objects but you also do not want to allow everything. There are some guidelines which no one should be allowed to break. Exactly this job does the static type system: While the compiler does not compile code doing something forbidden (means: passing wrong arguments to a method, calling a non existing method), interfaces and inheritance give you the freedom you need.

Summarizing this part, we can say that the strongly typed languages took one way in order to force some guidelines: They make great demands on the programmer when he is allowed to do what.

So even if they hinder the developer in some situations, in my personal opinion their advantages are bigger in most scenarios: Your application gets more stable by leaving some parts of its – well, let’s say – “testing” (or rather: functionality proving) the compiler. So there is one factor less you have to care about at runtime: Well written applications use casts very rarely and expose common functionality in interfaces so that they reach a bit of the “dynamic character” of duck-typing. You just give away a part of your responsibility allowing you to focus on the real problems.

Back to the topic

I hope you read our little trip to that topic carefully. But why did we go it?

After using Code Contracts for a while now, I would say: It’s just the same with them. Contracts are an extension of the static type system – they make some parts of it more strict.

For example, the very common problem with null: Languages like Spec# go their own ways by introducing a new kind of types: Non-Nullable-types. As we do not have them in C# currently, we are dependent on real code to close this “gap” in our type system.

Going one step further: Indices. Looking at the plain generic collections like List<T>, we see that the static type system did its job already: We can not use a string or a FileStream for example to get an item of the collection. We have to use a number; more precisely an Int32.

In both scenarios, Code Contracts are the solution: Just formulate appropriate preconditions and your methods are “secure”.

In order to generalize it, take a look at those two statements:

You can only call the method Foo on objects of type Bar passing a Baz.

You can only call the method Foo on objects of type Bar whose Name property is not null passing a Baz being not null whose Property property is greater equal 5.

Where is the difference between them? In principle, there is no; they are both requirements for the method Foo.Bar. Looking at the last sentence, however, you will see that the type system of C# is not able to check those conditions – they might change during runtime.

So the capabilities of C#’s type system are exhausted: Even if the documentation says that we are not allowed to pass values below zero, we are still able to. There is no one denying this during compile-time. If we made a mistake, it will show up at runtime only.

Preconditions

This, however, can be a problem: There might be cases where only values within a well-defined value range are allowed. If we introduced a class for each of them, we would have billions of really simple types only there to validate something. And still, the problem with dynamic value ranges could not be solved.

It would be really great to let the state of an object be part of the type system. In contrast to the actual type, this state would change during runtime and we could not always rely on specific behavior. This is a big difference to the known type system: You can always rely that there is e.g. a method Foo accepting a string and returning an integer. So only specifying types is not enough – we need to express which are valid states for a parameter. That’s exactly what preconditions do.

What are postconditions then?

On the other hand, we have to be able to say how the state changes: After calling a method it may be completely different. If we set a property’s value – does this affect the state? Postconditions can be what we are looking for; they describe the changings in the state of an object. Sometimes, new object are included, too: Postconditions say everything about return values and newly instantiated objects.

Furthermore, they inform about conditions implied by others without influencing the concrete implementation.

They give us the assurance what we are allowed to do meaning which preconditions we can fulfill at a specified moment. Without the postconditions, we would be quite lost: We would knew that there are guidelines we have to follow but we did not know, how to follow them. Thus, in comparison to preconditions, postconditions are something really “new” to us – they have no equivalent in today’s static type system. You surely never wrote an object where the compiler denies calling “Foo” until “Bar” is called.

Do Code Contracts really solve this problem?

Simple answer: No. However, they are “better than nothing”. I would say that they are a very careful step into the right direction. In my opinion, this step is too careful.

Looking at Spec# (I have to say that I did not use it yet, however, I read much about it) with its built in language constructs to formulate Contracts, you will see that there are more reasoned solutions: If violating them, code often won’t compile. That would be a really, really nice solution. Because of this, I can not understand, why Microsoft discontinued them.

What are Code Contracts then?

I already mentioned: They are a standalone extension to the static type system. Although they do not extend it physically, they do logically. So they do not redundantize unit testing.

This sentence may sound not really revolutionary or that important, but let me tell you it is. Keeping it in mind, you know what to use as pre- and postconditions. Do not understand this wrong: There will never be the perfect solution – there are always many roads leading to Rome.

This implies…

For example, it embodies what intention they do not conduce: Testing of the implementation. So Contracts should be not connected to the actual logic or implementation behind a method; they should be formulated at “interface-level”.

If you like checklists – here you are. Contracts have to be…

  • Simple. Keep Contracts as simple as possible – make them not too complicated.
  • Easy to check / performant to check.
  • Near to the object. It’s the best to have Contracts like foo.IsValid, this.Count > 0 or foo.Contains(bar).
  • only about an object’s state. Use them to require and guarantee state information, not to test implementation.
  • oriented at the interface – not at the implementation.
  • enough. Do not hesitate to write postconditions; even if you think that something is really clear.
  • not too much. Do not guarantee things a specific implementation might not be able to cover. Think twice before requiring something – is it really necessary?
  • comprehensible. Every pre- and postcondition should be logical – the user should not wonder about their meanings
  • not using any mathematical operators
  • not directly validating arguments expect of really required things – if there is more complicated validation required, they should delegate this to another method

Pre- and postconditions formulated using Code Contracts should only cover semantics and not any logic. It can be very hard to differentiate between those two terms; in many cases they will seem to merge seamlessly.

It can be really, really difficult to evaluate whether a pre- / postcondition is abstract enough or not.

Example

Think of a bank account Account with the properties Balance, CanOverdraw and IsLocked and the method Transfer(Account other, decimal money).

Which pre- and postconditions would you apply to the members?

Now look at my version and pay attention which pre- and postconditions I did not wrote:

public abstract class IAccount
{
    public decimal Balance
    {
        get
        {
            Contract.Ensures(this.CanOverdraw || Contract.Result<decimal>() >= 0);
        }
    }
    public bool CanOverdraw
    {
        get { }
    }
    public bool IsLocked
    {
        get { }
    }

    [Pure]
    public bool HasEnoughMoneyForTransferTo(IAccount second, decimal money)
    {
        Contract.Requires(second != null);
        Contract.Requires(money > 0);
    }

    public void Transfer(IAccount second, decimal money)
    {
        Contract.Requires(!this.IsLocked);
        Contract.Requires(second != null);

        Contract.Requires(!second.IsLocked);
        Contract.Requires(money > 0);
        
        Contract.Requires(this.HasEnoughMoneyForTransferTo(second, money));


        Contract.Ensures(this.Balance < Contract.OldValue(this.Balance));
        Contract.Ensures(second.Balance > Contract.OldValue(this.Balance));

        Contract.Ensures(this.IsLocked == Contract.OldValue(this.IsLocked));
        Contract.Ensures(second.IsLocked == Contract.OldValue(second.IsLocked));

        Contract.Ensures(this.CanOverdraw == Contract.OldValue(this.CanOverdraw));
        Contract.Ensures(second.CanOverdraw == Contract.OldValue(second.CanOverdraw));
    }
}

Did you notice I do not have any Postconditions like: this.Balance = Contract.OldValue(this.Balance) – money or second.Balance = Contract.OldValue(second.Balance) + money?

The reason is simple: That would cover more the implementation than the interface. In the future, there might be cross-boarder transactions for which the user has to pay. So our postcondition would be broken. Therefore, we want to test the interface: Saying that the source account has less money after the transaction than before and the destination account more than before, we keep everything flexible, abstract and logical.

Another point is that there is no preconditions like this.CanOverdraw || money < this.Balance. Again, that would be too much logic – validation like that is part of our application’s business code; it’s definitely not part of the Contracts. However, we want to cover this case: So we introduced a method HasEnoughMoneyForTransfer – we just require that it returns true and our contracts are complete.

However, an important precondition is that we do not accept negative values for money. They would simply be wrong as you will never be able to earn money by transfering negative amounts of money.

I hope you got a idea between "right" and "wrong" Contracts; its – as said before – really difficult to find good ones (for me, too).

Example 2

This a example is a real-world example, it comes by tobi from a comment to Part 4: Writing down Pre- and Postconditions: He asked my how to formulate postconditions for a Html-encoding class; special characters could be either encoded as hex or with their special aliases (e.g. &amp; &lt; …).

Now writing postconditions like input != "<" || (Contract.Result<string>() == "&lt;" || … would be a wrong approach: Contracts would be misused to validate the implementation.

My solution was a postconditions that ensures that the result does not contain any "forbidden" characters. And that’s exactly what you expect from the class; it doesn’t matter to you how exactly the class solves this.

Conclusion

You saw: Contracts cover quite simple but very important things. They get only broken when there are real bugs in your application.

Contracts should be seen as an extension to the static type system. They do not redundantize unit testing as they should not cover the actual logic but semantic.

Questions? Ideas? Suggestions? Problems? Different opinions? Pleas let me know!

About these ads

3 Responses to “Contracts as a part of the type system? (No Interface Without Contract – Part 7)”

  1. DotNetShoutout Says:

    (Code-) Contracts as a part of the type system?…

    Thank you for submitting this cool story – Trackback from DotNetShoutout…

  2. Paddy3118 Says:

    What you describe as strong typing is a little loose. You probably mean what is commonly described as Strong as in the type checking, and Static for when the checking is done, meaning at compile time.

    Several languages are strongly typed, in that their are checks to make sure operations between dissimilar types are strictly enforced; but such checking is done at run time rather than at compile time.

    The opposite of Strong typing is Weak typing, were, for example, a language might allow the addition of a string and a integer – two dissimilar types, to give some “numeric” value.

    Here is an example of weak typing:

    myshell: perl -e ‘print “cat” + 2; print “\n”; print 2 + “dog”; print “\n”‘
    2
    2

    Oh, and since you don’t want to mention … … I’ll stop here. :-)

    - Paddy.

  3. winsharp93 Says:

    Ok – you are totally right.
    I have to admit that I did not really think about this difference – maybe as I am not really sure whether the “Contract Type” should be part of the “strong” type or only part of the “static” (means compiler checked in this case) type.

    Thanks for pointing that out!

    Cheers
    winSharp93


Comments are closed.

Follow

Get every new post delivered to your Inbox.

%d bloggers like this: