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?

Read the rest of this entry »

No Interface without Contract? – Part 6: Object Invariants

Invariants are a kind of postconditions which apply to all members. How to formulate them using Code Contracts?

In the previous part we got started using Microsoft Code Contracts and formulated first pre- and postconditions. We only looked at “simple” ones. In this posting you will learn what object invariants are and how they are connected with Code Contracts.

What are Invariants?

As anticipated in the introduction, invariants can be compared to postconditions valid for all members of a class. In fact, you are actually able to modulate them using Contract.Ensures(invariant) in each member.

However, they are more than simple postconditions – they are always valid, regardless of the object’s state. So invariants must never be broken during an object’s lifetime. Thus, other members can rely on them like on preconditions.

Read the rest of this entry »

No Interface Without Contract? – Part 4: Writing down Pre- and Postconditions

Contracts are important – we already saw this. What can we do that we always see them when coding?

In the previous part, we formulated pre- and postconditions for a sample class. However, we only have written them down in plain text.

So we are now finding out how to specify them in a more comfortable (and elegant of course 😉 ) way.

I will introduce five possibilities: Documentation, Exception / Assert based, Custom Checker Class, Attributes and Code Contracts.

Read the rest of this entry »

No Interface Without Contract? – Part 3: Finding Pre- and Postconditions

“If you give me a string not beeing null or empty, I will give you a number greater zero” – Pre- and Postconditions made easy.

In the previous part, we found out that pre- and postconditions improve the quality of our code.

Note: I primary announced that part 3 is about writing them down. However, while writing I realized that it is better to split up this part.


Let’s take a look at our sample class first:

Read the rest of this entry »

No interface without contract? – Part 2: About Pre- and Postconditions

Pre- and Postconditions: What they are, why you should use them and how they help you.

In the last part, the result was that we need something helping us to specify those kinds of “Implementation-Requirements”.

I already alluded to Pre- and Postconditions.

Read the rest of this entry »

No interface without contract? – Part 1: Why plain interfaces aren’t enough

An interface is an interface – why this is not always right.

What is an interface?

Wikipedia says:

Interface generally refers to an abstraction that an entity provides of itself to the outside.

In C#, interfaces are realized using the interface keyword. It is explained as follows:

An interface contains only the signatures of methods, delegates or events. The implementation of the methods is done in the class that implements the interface, […]

You have to separate between these two definitions:

Read the rest of this entry »