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.

Documentation

Having formulated the pre- and postconditions in plain text, a logical step would be writing them into the XML-Documentation.

Realization

Lets do this for Foo.Bar:

/// <summary>
/// ...
/// </summary>
/// <remarks>
/// <para>
/// <list>
/// <listheader>Preconditions</listheader>
/// <item><see cref="IsValid"/> must be true.</item>
/// <item><paramref name="index"/> must be greater equal 0 and less than <see cref="Property.Lenght"/></item>
/// </list>
/// <list>
/// <listheader>Postconditions</listheader>
/// <item>The return value is between 0 and 9.</item>
/// <item><see cref="Property"/> contains the string representation of the return value.</item>
/// <item>The string representation of the return value equals <see cref="Property[index]"/>.</item>
/// </list>
/// This method does not affect the state of this <see cref="Foo"/>.
/// </para>
/// </remarks>
public int Bar(int index)
{
    char value = this.Property[index];
    return Convert.ToInt32(value);
}

Advantages
  • Formulating pre- and postconditions as a part of the documentation is quite obvious – it seems to be a good place as every developer (should) look into the documentation before using a class / a member
  • Sometimes, language can be clearer than all code together
Disadvantages
  • Pre- and Postconditions are not checked at runtime. You have to trust the caller that he makes everything right. In addition, you don’t know, if your code breaks them.
  • Some formulations may be unclear
  • Going this way means very much work

Exception / Assert-base

The “classic way”: Using exceptions and Debug.Asserts.

Realization
public int Bar(int index)
{
    if (!this.IsValid)
        throw new InvalidOperationException("IsValid must be true.");
    if (index < 0
        || index >= this.Property.Lenght)
        throw new ArgumentException("index must be greater equal 0 and less than Property.Lenght ");

    char value = this.Property[index];
    int result = Convert.ToInt32(value);

    Debug.Assert(result >= 0 && result < 9, "The return value must be between 0 and 9");
    Debug.Assert(this.Property.Contains(result.ToString()), "Property must contain the string representation of the return value.");
    Debug.Assert(String.Equals(result.ToString(), this.Property[index]), "The string representation of the return value must equal Property[index].");

    return result;
}

Advantages
  • Runtime checks – if the code doesn’t comply with the pre- and postconditions you will notice very early.
  • Postconditions are only checked in DEBUG-Builds (Better performance in release version)
Disadvantages
  • The code gets fragmented – you need a variable result and have to check the postconditions after the “real” implementation
  • It’s not that easy to control whether pre- and postconditions should be checked (depending on the current configuration)
  • No possibility of “recursive” postconditions – two members use each other to specify their postconditions
  • Preconditions must be formulated negative – if you want index to be bigger 0 you will have to check against “index < 0” – while postconditions are formulated positive

Custom Checker Class

Instead using if-throw and Debug.Asserts, you can write your own “Checker Class”. A very simple one would look like the following:

public static class Checker
{
    public static void Precondition<TException>(bool condition, params object[] constructorArgs)
        where TException : Exception
    {
        if (!condition)
            throw (Exception) Activator.CreateInstance(typeof(TException), constructorArgs);
    }
    public static void Postcondition(bool condition, string message)
    {
        Debug.Assert(condition, message);
    }
}

Our Bar method now is:

public int Bar(int index)
{
    Checker.Precondition<InvalidOperationException>(this.IsValid, "IsValid must be true.");
    Checker.Precondition<ArgumentException>(index > 0 && index < this.Property.Length, "index must be greater equal 0 and less than Property.Lenght");

    char value = this.Property[index];
    int result = Convert.ToInt32(value);

    Checker.Postcondition(result >= 0 && result < 9, "The return value must be between 0 and 9");
    Checker.Postcondition(this.Property.Contains(result.ToString()), "Property must contain the string representation of the return value.");
    Checker.Postcondition(String.Equals(result.ToString(), this.Property[index]), "The string representation of the return value must equal Property[index].");

    return result;
}

Advantages
  • Runtime checks
  • Very good control: You only have to change Checker to control what should happen if a pre- or postcondition fails
  • Checks centralized
Disadvantages
  • Code gets fragmented
  • “Recursive” conditions cause problems

Attributes

Another interesting possibility is aspect orientation using Attributes. As I did not go that way yet, I only have dummy-code:

[Precondition("index > 0 && index <= this.Property.Lenght", "index must be greater equal 0 and less than Property.Lenght")]
[Precondition("this.IsValid", "IsValid must be true.")]
[Postcondition("$result$ >= 0 && $result$ < 9", "The return value must be between 0 and 9")]
[Postcondition("this.Property.Contains($result$.ToString())", "Property must contain the string representation of the return value.")]
[Postcondition("String.Equals(result.ToString(), this.Property[index])", "The string representation of the return value must equal Property[index].")]
public int Bar(int index)
{
    char value = this.Property[index];
    int result = Convert.ToInt32(value);

    return result;
}

Advantages
  • Separation of code and pre- / postconditions
  • only really “necessary” code is written / no if-throw constructs
  • easy access to the return value
  • fully controllable runtime checks
Disadvantages
  • No IDE support when formulating pre- and postconditions (as Attributes do not allow code as parameters)
  • A rewriting tool is required
  • Pre- / Postconditions are formulated language specific (C#, VB etc.)
  • “Complex” checks may look quite strange or are not possible

Code Contracts

Now how would Bar look using Code Contracts?

Just look at the code – I will explain it in the next part.

[Pure]
public int Bar(int index)
{
    Contract.Requires<InvalidOperationException>(this.IsValid, "IsValid must be true.");
    Contract.Requires<ArgumentException>(index > 0 && index < this.Property.Length, "index must be greater equal 0 and less than Property.Lenght");

    Contract.Ensures(Contract.Result<int>() >= 0 && Contract.Result<int>() < 9, "The return value must be between 0 and 9");
    Contract.Ensures(this.Property.Contains(Contract.Result<int>().ToString()), "Property must contain the string representation of the return value.");
    Contract.Ensures(String.Equals(Contract.Result<int>().ToString(), this.Property[index]), "The string representation of the return value must equal Property[index].");

    char value = this.Property[index];
    int result = Convert.ToInt32(value);

    return result;
}

Advantages

  • Code and pre- / postconditions are quite separated
  • Easy access to return values
  • Good control over runtime checking
  • Probably good support in the future as included in .NET 4.0
  • Static checker available
  • Supports recursive conditions

Disadvantages

  • VS integration only with VS 2008 / 2010
  • Rewriting required (build slowdown)
  • CTP Stadium / some bugs
  • Problems in multithreaded environments (only limited usefulness)

Conclusion / Outlook

We saw that there are few possibilities to formulate pre- and postconditions.

Code Contracts will be the tool of choice in the next parts as they will be included in .NET 4.0. So its likely there will be more tools supporting them in the future. This could include tools for automatic creation of documentation, unit testing tools and maybe even the ReSharper (that’s just a guess of mine).

In the next part we will get started using Code Contracts and explain their most important aspects.

DotNetKicks Image
About these ads

6 Responses to “No Interface Without Contract? – Part 4: Writing down Pre- and Postconditions”

  1. tobi Says:

    do you have any ideas on what postconditions to choose? image a function HtmlEncode: it could encode angle brackets with < or it could encode them using #hex; what should the author of the HtmlEncode function choose as a postcondition?

  2. tobi Says:

    in my previous comment, the < was supposed to be & lt ;. seemingly the blog software did not encode it. test: alert(‘bad blog software’);

  3. tobi Says:

    unfortunately it is impossible to leave html tags in the comments. it would be worth another blog entry to decide if you should strip dangerous html or encode it.

  4. winsharp93 Says:

    >> it could encode angle brackets with &lt; or it could encode them using #hex; what should the author of the HtmlEncode function choose as a postcondition?
    Well – I think postconditions should not go that far and cover the “real logic” behind a method.
    They do not redundantize testing! In my opinion, this would be part of a unit test.
    As postconditions in this case, I would use that the return value is neither null nor empty (and things like that).
    Another, important one, could be that the result does not contain characters like ‘<’, ‘>’ …

    >> unfortunately it is impossible to leave html tags in the comments.
    You can escape the ampersand and write &amp;lt; (I had to do the escaping, too).
    However, there seems to be no setting to change behaiviour if there are HTML expressions like those. If there is one, please let me know where it is.

  5. tobi Says:

    guaranteing that the result does not contain < is a smart way to do it i guess.

  6. DotNetShoutout Says:

    No Interface Without Contract? – Writing down Pre- and Postconditions…

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


Comments are closed.

Follow

Get every new post delivered to your Inbox.

%d bloggers like this: