Code Contracts #8: Sandcastle integration

Release 1.2.20903 (4 Sep 2009) of Code Contracts comes with a nice integration of contracts on classes and methods into Sandcastle documentation! By this, Code Contracts achieve an important goal: real „checked documentation“. This short article gives an overview of how to get your Sandcastle installation to handle contracts.

1) Install Sandcastle (+DocProject)

At first, of course you need a valid Sandcastle installation. Just go to the Sandcastle project page, download the latest release and install it. I recommend installing DocProject for Sandcastle and HTML Help Workshop and Documentation as well. This gives you a nice Visual Studio integration for creating documentation by Sandcastle.

2) Patch Sandcastle with Code Contracts files

Code Contracts documentation syntax is currently not included in the Sandcastle project. In order to make Sandcastle aware of the Code Contracts documentation items, you have to patch the Sandcastle installation with the Code Contracts files. For this, there exists a folder „Sandcastle“ in the Code Contracts installation directory (default is „Program Files\Microsoft\Contracts\Sandcastle„), which contains a file „Sandcastle.zip„.

If you’ve installed Sandcastle from the MSI package, just copy the contents from the „msi\vs2005“ folder of the UIP file to the following location of your Sandcastle installation: „Program Files\Sandcastle\Presentation\vs2005\„. Now you’re done and ready to generate documentation for your contracts!

3) Set up your project

First, if you want to generate documentation for a project in Visual Studio, go to the project properties and in the „Build“ option pane, check the XML documentation file option:

Activate the "XML documentation file" option

Then, to get the contracts injected into the generated XML doc file, go to the „Code Contracts“ option pane and select both the Build a Contract Reference Assembly and the Emit contracts into XML doc file options:

Select generation of Code Contracts documentation

Now, when you build your project, first the documentation of your project’s components will be created as XML file and then the contracts documentation will be injected in the same file.

4) Create your documentation!

For demonstation purposes, I’ve generated a project (including a new solution) AccountExample in Visual Studio, which holds just one class Account. This example class contains some contracts and looks as follows:

/// <summary>
/// Represents an account, to which you can deposit and from which you can withdraw money.
/// </summary>
public class Account
{
    private float _balance;
    /// <summary>
    /// The current balance of the account.
    /// </summary>
    /// <value>The account's balance.</value>
    public float Balance
    {
        get { return _balance; }
        private set
        {
            Contract.Requires(value >= 0);
            _balance = value;
        }
    }

    [ContractInvariantMethod]
    protected void ClassInvariants()
    {
        Contract.Invariant(_balance >= 0);
    }

    /// <summary>
    /// Initializes a new instance of the <see cref="Account"/> class.
    /// </summary>
    /// <param name="balanceInitial">The initial balance, which will be set.</param>
    public Account(float balanceInitial)
    {
        Contract.Requires(balanceInitial >= 0);
        Contract.Ensures(Balance == balanceInitial);

        Balance = balanceInitial;
    }

    /// <summary>
    /// Deposits the specified amount to the account.
    /// </summary>
    /// <param name="amount">The amount to deposit.</param>
    public void Deposit(float amount)
    {
        Contract.Requires(amount > 0);
        Contract.Ensures(Balance == (Contract.OldValue(Balance) + amount));

        Balance += amount;
    }

    /// <summary>
    /// Withdraws the specified amount from the account.
    /// </summary>
    /// <param name="amount">The amount to withdraw.</param>
    public void Withdraw(float amount)
    {
        Contract.Requires(amount > 0);
        Contract.Requires(amount <= Balance);
        Contract.Ensures(Balance == (Contract.OldValue(Balance) - amount));

        Balance -= amount;
    }
}

Moreover, I’ve added a new DocProject to my solution, where I’ve chosen the „AccountExample“ project for generating the documentation from. With that we’re ready to roll!

When building the whole solution, first the assembly of the „AccountExample“ project is built. In this step, the following XML documentation file is extracted as well (note the injected contract tags – requires, ensures and invariant):

<?xml version="1.0"?>
<doc>
  <assembly>
    <name>AccountExample</name>
  </assembly>
  <members>
    <member name="T:AccountExample.Account">
      <summary>
            Represents an account, to which you can deposit and from which you can withdraw money.
            </summary>
      <invariant>_balance >= 0</invariant>
    </member>
    <member name="M:AccountExample.Account.#ctor(System.Single)">
      <summary>
            Initializes a new instance of the <see cref="T:AccountExample.Account" /> class.
            </summary>
      <param name="balanceInitial">The initial balance, which will be set.</param>
      <requires>balanceInitial >= 0</requires>
      <ensures>Balance == balanceInitial</ensures>
    </member>
    <member name="M:AccountExample.Account.Deposit(System.Single)">
      <summary>
            Deposits the specified amount to the account.
            </summary>
      <param name="amount">The amount to deposit.</param>
      <requires>amount > 0</requires>
      <ensures>Balance == (Contract.OldValue(Balance) + amount)</ensures>
    </member>
    <member name="M:AccountExample.Account.Withdraw(System.Single)">
      <summary>
            Withdraws the specified amount from the account.
            </summary>
      <param name="amount">The amount to withdraw.</param>
      <requires>amount > 0</requires>
      <requires>amount <= Balance</requires>
      <ensures>Balance == (Contract.OldValue(Balance) - amount)</ensures>
    </member>
    <member name="P:AccountExample.Account.Balance">
      <summary>
            The current balance of the account.
            </summary>
      <value>The account's balance.</value>
      <setter>
        <requires>value >= 0</requires>
      </setter>
    </member>
  </members>
</doc>

In a second step of the build process, the DocProject generates the documentation for the „AccountExample“ project by taking its XML documentation file. When finished, we’ll have a nice CHM file with the documentation of our example project.

In this documentation we can see our contracts now. On class level, we have our invariant:

Class invariants in Sandcastle documentation

And on method (+properties) level, we get the pre- and postconditions:

Method contracts in Sandcastle documentation

Conclusion

As you can see, contracts in documentation are really valuable. Including them in Sandcastle documentation brings the claim of „checked documentation“ to life! This really helps other developers to understand the intent of your classes by looking at the documentation. And by automatically generating documentation out of your code-based contracts, you can be sure that docu and code do not run out of sync. This really puts more value on Code Contracts and is a real practical advantage!

kick it on DotNetKicks.com

New Code Contracts Release

On September 4th, Microsoft has made a new Code Contracts release available. Release 1.2.20903 (4 Sep 2009) comes among others with the following changes:

  • Inclusion of Code Contracts into Sandcastle documentation! Thereby, Code Contracts achieve a full state of „checked documentation“.
  • Improvements of the dynamic and static checker
  • More contracts on core .NET framework assemblies
  • Silverlight 3 support
  • Many bugfixes on community feedback

Important hint: there are no API changes! Thus existing examples and blog posts on Code Contracts remain valid. Have a look at the release notes for a full list of changes.

Please keep posting your comments and suggestions for improvement on the Code Contracts forum.

Code Contracts #7: Relation to Guard classes

Hey guys. After two months of many things to do I come back again with an article to Code Contracts. This day’s topic are guard classes and how they relate to Code Contracts.

Recently my colleague AJ posted a really nice article about guard classes. He’s the first one who explained the topic as a whole and showed the advantages of using guards. In short version, guard classes in this context are mainly about guarding against passing invalid arguments into class methods.

For example, without having a guard, you would check method arguments that way:

public void FooMethod(string arg)
{
    if(arg == null)
        throw new ArgumentNullException("arg");
    if(arg == "")
        throw new ArgumentOutOfRangeException("arg");
    ...
}

While this approach is defensive and can lead to less errors, it’s quite ugly to have those checks defined in every method directly. First, the if-clauses are polluting the method’s body. The if and throw keywords are too much information at this location. Second, for example if a string should not be empty, it’s obvious that it may not be null as well. And what if we want to log those exceptions or do something else (for example inform an administrator)? Here come guard classes into play. The aspect of throwing exceptions and perhaps do something before that is outsourced into a separate utility class Guard. With that on hand, the example from above would transform into:

public void FooMethod(string arg)
{
    Guard.AssertNotEmpty(arg, "arg");
    ...
}

You can find the guard’s AssertNotEmpty() method in AJ’s post.
The guard encapsulates the argument validation as cross-cutting-concern and makes it exchangable. The call clearly expresses what is done at that point and thus it’s better separated from the core logic of the method. It concentrated on the main purpose and not on the implementation details.

Well, how are method guards fitting with Code Contracts or Design by Contract (DbC) at the whole? The simple answer: method guards are nearly equivalent to preconditions in DbC! They express the basic conditions on level of physical constraints, under which a method is expected to work correctly.

With Code Contracts, in .NET 4.0 we don’t need an explicit Guard class any longer. The above example can be realized with Code Contracts as:

public void FooMethod(string arg)
{
    Contract.Requires(arg != null, "arg should not be null");
    Contract.Requires(arg != "", "arg should not be empty");
    ...
}

As with guard classes, this ‚precondition block‘ abstracts the implementation details of the check itself and it’s purpose is obvious, thus leading to a separation of the core logic, if you look at the method with developer’s eyes.
One ‚problem‘ remains with this example. With the guard class we’ve had the chance to define individual methods, that fit our needs. For example, it checks for empty strings that they aren’t null as well (please take aside String.IsNullOrEmpty() for a moment) or it puts in logging logic. Code Contracts gives us just the Contract.Requires() method, which doesn’t have these abilities at first. If you have many repeating individual checks I suggest to use a separate static class that contains all of your needed checks as methods, that return a boolean value if the check passes. Those methods must be declared [Pure] in order to be used in contracts, thus they must be free of observable side effects. With such a class Check, the example above would look as follows:

public void FooMethod(string arg)
{
    Contract.Requires(Check.NotEmpty(arg), "arg should not be null or empty");
    ...
}

Check is simple in this case:

public static class Check
{
    [Pure]
    public static bool NotEmpty(string arg)
    {
        return ((arg != null) && (arg != ""));
    }
}

Alternatively, you could define extension methods on the datatypes, that should get individual checks. This frees you from a dedicated class, that must know all of the datatypes to check.

For doing additional stuff like logging on fail of a precondition, you get the ability to plug in your own custom contract runtime class. Please read the Code Contracts documentation for detailed information on this subject.

Thus, Code Contracts give you the same advantages as guard classes. But moreover, there are clear additional benefits!
First, you are free to change the check behavior of your preconditions by configuration. The Code Contracts tools allow you to perform checks in debug mode only or even in the release build. Furthermore you can define, if you want the program to Assert or to throw an exception, if a precondition check fails and so on. Thus, you get a high flexibility to adapt Code Contracts to your own needs.
Second, Code Contracts give you the ability to directly extend the interface of your class. It allows you to define contracts on abstract classes and interfaces, that will be automatically taken into concrete implementations.
Third, contracts of all kinds are derived to every subclass of the class, where you have defined them. By that, you aren’t allowed to add any precondition in your subclass with Code Contracts, but you are able to define additional postconditions or invariants. Thereby, the compliance of the Liskov Substitution Principle is enforced on the level of contracts.
Fourth, don’t forget that DbC is a design principle and goes beyond the technical implementation on the level of guard classes.
Fifth, precondition checks allow tool support. They can be included in the run of the static checker and even the automatic test generator Pex is aware of contracts and uses preconditions of your methods as test oracle.

That’s it for now. In conclusion, Code Contracts go beyond guard classes and because they are a core component of .NET 4.0, you don’t need custom guard classes any longer. Simply use contracts instead…

kick it on DotNetKicks.com

new CloudApp(): Rating Stress Simulator

Recently, Microsoft came up with the new CloudApp() Contest. This competition encourages developers all over the world to create some applications on Microsoft’s Azure platform that make use of the cloud and emphasize the cloud computing benefits. While the U.S. winners are already chosen, the international contest will be open for community vote during 10th July and 20th July.

For this competition and as part of our overall technology partner strategy, my company SDX AG has built up a team to develop an Azure-based business application showcase. Our team developed a business scenario and has taken advantage of Windows Azure and Silverlight to realize this scenario in the cloud. I’ve had the chance to take part in the brainstorming process and joined the team for some development tasks during the last days…

The business story

Since my company has core competences in the financial sector, the business scenario targets this area as well. The application realizes a rating stress simulator for banks. What is this about? That’s the story: Financial institutes cannot provide credits freely. Each credit must be backed with a certain amount of money, depending on a calculated risk (rating for a credit user).

Functionality

Our Azure application is a simple showcase on base of this business scenario. It allows users to run a financial stress test which calculates capital buffers, that are needed to withstand selected situations (such as a recession) over some period of time. After the stress test is run, the user can view the results of the calculation visually. The included algorithms are very simple, but they verify the architectural model of our cloud application and bring it to reality.

Benefits

A bank in need for this functionality has real benefits of letting the application run in the cloud. Such a stress test is not computed continuously, but runs on a periodical cycle, e.g. weekly or monthly. Thus the processing power and storage capacity has a short peak where the server CPUs get busy, but the rest of the time they remain idle. By running the application in the cloud, a bank has no need for additional servers in its datacenter to buffer the computational peaks of the stress test. Thereby, the infrastructure and administrative costs can be clearly reduced.

Try out and vote!

Of course, you are able to run the application for yourself and try out its functionality. By this URL, you can start the Silverlight application: http://ratingsimulator.cloudapp.net.  I encourage you to read the introductory information on the first page to prepare yourself for the application and to get more background information. Then play around, create some scenarios with a certain number of credits and let the calculation run in the cloud. Afterwards you can view the stress test results in a summarizing diagram.

If you like our little application, we would be very glad if you vote for us. You can do that with the following link: [voting closed]. Thanks a lot for your support!

new Cloudapp() - Rating Stress Simulator

My colleague AJ has published a blog post about this as well: new CloudApp()

kick it on DotNetKicks.com

My Top-3 development tools

Currently, MSDN Germany arranges a blog-parade and is asking developers to disclose their top-3 development tools. I will follow this request, so here are my current top 3 development tools, that make the developer’s life really easier. They are to see in addition to Visual Studio 2008. VS is a really wonderful tool and I do not want to miss Intellisense, TFS integration debugging support anymore. But it’s not perfect and here those tools come on stage:

  1. Jetbrains ReSharper:
    I just started with this brilliant tool and from the first moment on I loved this beautiful piece of software. ReSharper is a Visual Studio plugin, that helps you on managing, refactoring and navigating your code more easily. Visual Studio has a lack of functionality in these areas and ReSharper bridges the gap here. Some examples: if you are heavily using interfaces, you will have pain when navigating through your code with Visual Studio alone, because by pressing F12 you will only come to the interfaces, but not to the implementations. With Resharper you can press Ctrl+Alt+B and come to the direct implementation, if there is just one. If there are more, you will have the choice to navigate to one of them. Other nevigation features include: go to declaration, implementation, inheritors, find usages, … – it really increases productivity! Another example are the great refactorings. Visual Studio has to hide in shame in comparison. One remark: CodeRush Xpress is another nice refactoring tool, which supports you on code navigation, too. It’s kind of limited in the free Xpress edition, but it’s always nice to have, if there’s no chance for the ReSharper.
  2. NDepend Pro:
    As another great tool, NDepend helps you in analyzing your code or existing code bases from other developers. It shows you dependencies between solution projects and creates default queries on the code, while supporting many popular code metrics. NDepend can be run on projects without Visual Studio, but also smoothly integrates into VS context menus. Furthermore, you are able to freely define your own code queries, for example to find all classes, that have more than a certain number of lines or methods, that have a high degree on cyclomatic complexity. By supporting the CQL (code query language), such queries are very flexible and quickly created.
  3. GhostDoc:
    Document your code! Many programmers and even developers have problems with this demand. GhostDoc supports you in this task. It integrates into Visual Studio and if you press Shit+Ctrl+D on any piece of code, you get a documentation template, that’s created automatically by use of the component’s name and the data type (or return type). In some cases this default documentation is sufficient, but mostly you have to adapt it. GhostDoc helps you in giving you a template, but for documenting what your code does you are responsible on your own! Don’t rely on automatic docu, since this isn’t doing the job alone. Additionally, GhostDoc can assist you on changes of your code. If you change the signature of an earlier documented method, GhostDoc can look on the changes and include new parameters to the docu respectively delete old ones. I don’t wanna miss this brilliant tool and the best: it’s for free!

That’s it from my view. I really missed more tools like .NET Reflector, but those are just my top-3. I’m agog: what are your top-tools in development and why?

Code Contracts #6: Modelling constraints and state

(Note: this article has been updated on 2009/05/16 by replacing the example and adding some more information)

Modelling constraints on class properties and valid state of classes explicitly is an interesting topic and sometimes I catch myself being frustrated by the lack of handling these aspects through current programming languages. With „constraint“ I mean a condition on one class property or on a set, which equals a subset of the properties for the class. The same is true for the „state of a class“. Periodically I run into situations, where I have for example two properties, whose values depend on each other. And what I want is to express explicitly, that when property 1 is in state X, then property 2 must be in state Y and vice versa and that this constraint on those properties (their depending state) mustn’t be broken!

Let’s consider a (very) little example in form of the following class MinMax:

public class MinMax
{
    public int MinValue { get; set; }
    public int MaxValue { get; set; }
}

Not too impressive, isn’t it? 😉 But as you can imagine, there is one obvious constraint: MinValue <= MaxValue. Two other constraints are related to each property for itself – they mustn’t be less than 0: MinValue >= 0 and MaxValue >= 0 must be true. If those 3 conditions are true, then the class can be seen to be in a valid state. And in this case, we want to ensure this valid state all the time. The question follows quickly: How to model these constraints? Normally, you as programmer wouldn’t be very concerned about that. For example, in the setters of MinValue and MaxValue, you would check the constraints and throw an exception, if they don’t hold:

public class MinMax
{
    private int _MinValue;
    public int MinValue {
        get { return _MinValue; }
        set
        {
            if (value %gt; MaxValue)
                throw new ArgumentException("value can't be greater than MaxValue");
            if (value < 0)
                throw new ArgumentException("value can't be less than 0");

            _MinValue = value;
        }
    }

    private int _MaxValue;
    public int MaxValue
    {
        get { return _MaxValue; }
        set
        {
            if (value < MinValue)
                throw new ArgumentException("value can't be less than MaxValue");
            if (value < 0)
                throw new ArgumentException("value can't be less than 0");

            _MaxValue = value;
        }
    }
}

There’s an even better way, when you use a Guard class for that. Better, because you’ve outsourced the exception throw into the guard and you can do additional things there like logging something:

public class MinMax
{
    private int _MinValue;
    public int MinValue
    {
        get { return _MinValue; }
        set
        {
            Guard.Against<ArgumentException>(
                value > MaxValue, "value can't be greater than MaxValue");
            Guard.Against<ArgumentException>(
                value < 0, "value can't be less than 0");

            _MinValue = value;
        }
    }

    private int _MaxValue;
    public int MaxValue
    {
        get { return _MaxValue; }
        set
        {
            Guard.Against<ArgumentException>(
                value < MinValue, "value can't be less than MaxValue");
            Guard.Against<ArgumentException>(
                value < 0, "value can't be less than 0");

            _MaxValue = value;
        }
    }
}

public static class Guard
{
    public static void Against<TException>(bool assertion, string message)
        where TException : Exception
    {
        if (assertion)
            throw (TException)Activator.CreateInstance(typeof(TException), message);
    }
}

So it seems to be pretty easy to handle our constraints, right? Please don’t just take this stupid example into account. Imagine more complex cases, where you have numerous constraints on your class properties (one property or more than one depending properties), which aren’t far so obvious as in this example. Can you imagine the problems which arise, when you model them implicitly?

What if we would have a mechanism to model such (depending) property constraints explicitly, thus expressing valid class states? This would have some interesting advantages. First it helps you as programmer in creating and extending your class by ensuring that the constraints are maintained. Second it works as checked documentation for your code. If other programmers are extending your class, they would be aware of the constraints. By making things explicit and code-checked, it’s ensured that your classes are in valid state at every time by watching the defined constraints. Take MinMax as an example yet again. If you or another programmer is extending the class, you are not forbidden to write _MinValue and _MaxValue directly, thus going around the „state maintainers“ in form of the setters in MinValue and MaxValue and the calls to Guard. This example is small enough to not getting confused, but in more tricky cases the class could be left easily in an inconsistent state and yield more problems. An explicit model could lead a way out of that! Third when you distribute your components to third-party users, you would yet again reveal your intent by making the constraints of the class explicit. Users would be aware of them and could easier reproduce the behavior of your components. Hence there’s a much better chance that they use your class in a proper way from the beginning.

Do we have a mechanism to model such things? First if we think about class state, perhaps the GoF State pattern comes into mind, but that doesn’t fit our needs. It doesn’t have the power to make constraints explicit and model valid class state. But we can use Code Contracts for that! Object invariants (= invariants on classes) are exactly what we need. Object invariants give us the power to model constraints on classes explicitly, check them at compile and/or runtime (using the static or dynamic checker) and moreover allow us to define them on interfaces and abstract classes! Implementing/deriving classes must maintain the defined invariants and are allowed to make them stronger (but not weaker). So how would our MinMax-class look with that? Let’s see:

public class MinMax
{
    public int MinValue { get; set; }
    public int MaxValue { get; set; }

    [ContractInvariantMethod]
    protected void ClassConstraints()
    {
        Contract.Invariant(MinValue >= 0);
        Contract.Invariant(MaxValue >= 0);
        Contract.Invariant(MinValue <= MaxValue);
    }
}

That’s really small and seems to be pretty, doesn’t it? With the ContractInvariantMethod we can declare a method that contains the invariants/constraints of the class, which must be maintained by every class method (including get/set on properties). This method and its checks are run on exit of every other class method. With Contract.Invariant() you’re able to define an invariant. It doesn’t matter if there are simple cases as here or more complex cases on depending properties (for example implications) – every boolean expression can be modelled with that.

However somebody could find some issues with this example, so let’s explain. The above code is pretty, because the constraints are outsourced to one single method (thus avoiding redundancies) and you haven’t to take care of calling this method everytime (because Code Contracts will call it for you on exit of every other method).
As first issue, callers (clients) of the MinValue.set and MaxValue.set methods don’t see directly which values are allowed, because it’s not part of the method contract (the preconditions on the setters). In this example it’s ok, because he can look at the invariants (the contract of the whole class) and see, which values are allowed. So this issue is weak here, but in other method cases you really have to duplicate invariants with preconditions, what is some kind of ugly.
Second, the static checker will not be happy with that code, because it’s aware of that you can provide some invalid value in the setters. That’s an issue of Code Contracts itself and I hope the team will come up with some further development to handle this case automatically. So this issue is weak as well.
The third issue seems to be stronger. If an invariant is broken and hence a ContractException is thrown, the wrong value will remain in the current MinMax instance, if you handle the exception outside with try/catch (MinMax is left in an invalid state). If you don’t use the object anymore, that’s no problem, but else you have no chance to go to the state before the exception was thrown, except you’re handling that on your own in the caller/client. Is this a really good issue? Again, it’s not. This issue goes away, if we look at the purpose and behavior of DbC for this case. In DbC the client is responsible for ensuring preconditions when calling a method and if it comes to properties, he has to respect the invariants, too. If the client breaks a method’s contract, then the method itself is not obligated to ensure defined behavior – it’s simply undefined. And since contracts should be compiled out from the release version (while debugging and testing has been run before), that’s no problem at all. The break of a contract means the presence of a bug. The client should not handle such a case (handle the bug) by catching the exception and then further using the object. The object should be thrown away and the client must take care to call the method in a proper way.
As you can see, there are no definite issues with this example. Fortunately for true, because including preconditions in every setter would have meant to duplicate assertions as preconditions and invariants and this would destroy the advantage of having minimal check redundancies compared with the concept of defensive programming.

This article has shown some interesting aspect of Code Contracts. Modelling constraints (on (depending) properties) and valid class states is not handled very well by programming languages and easily yields to various coding problems, since your intention isn’t made explicit and valid class state isn’t checked automatically. Code Contracts can help us in this case very well by the use of object invariants. One more time making things explicit helps you as programmer and other programmers that use or extend your components.

kick it on DotNetKicks.com

Code Contracts #5: Method purity

After getting some things done, now I’m returning to Code Contracts. In the first parts of this series I gave you some basic information about Code Contracts, the static and dynamic checker, the code rewriter and how implications can be modelled. This day’s blog post comes up with another interesting aspect: method purity. There seems to be some misunderstanding on this term – I want to clear some clouds and show you what method purity means and which implications it has.

Code Contracts come with an attribute called [Pure] for decorating class methods (and by which you can declare a method as being „pure“). Method purity is a quality, expressing that the method is free of observable side effects. This means, it does not change the observable state on any objects seen by callers in some way. For example, pure methods do neither modify properties of a class nor reference type method arguments. Even the modification of a private field (which is not seen by callers directly) is prohibited, if class methods work with this field and return values, that depend on it. In this case the change of the field is indirectly reflected by a changed method return value, thus the observable state has changed! To summarize, mostly pure methods are only allowed to change objects that have been created after method entry.

The following code shows the simple class Point and gives you a short example of how to use Pure in declaration and pure method calls in contracts. The static and dynamic checkers will both be very happy with that 🙂 :

public class Point
{
    public int X { [Pure] get; set; }
    public int Y { [Pure] get; set; }

    public Point() { }

    [Pure]
    public double GetDistance()
    {
        return Math.Sqrt(X * X + Y * Y);
    }

    public void SwapXY()
    {
        Contract.Ensures(Contract.OldValue<int>(X) == Y);
        Contract.Ensures(Contract.OldValue<int>(Y) == X);
        Contract.Ensures(Contract.OldValue<double>(GetDistance()) == GetDistance());

        int temp = X;
        X = Y;
        Y = temp;
    }
}

(Perhaps not the best example, because we have redundant information in code and contracts in SwapXY() – that should not be the goal in most cases, but in this simple scenario it’s quite ok for demonstration purposes)

 

All methods that are called within a contract (pre-/postcondition etc.) must be declared pure. But why?

First it has a very certain reason: contracts like the Contract.Requires() and Contract.Ensures() assertions will not be evaluated in every execution and build configuration. For example, you can choose just to check pre-conditions, thus stepping over the post-conditions. I don’t need to explain, that methods with side effects in those post-conditions would be a messy thing. The execution results of your code would depend on the configuration of Code Contracts and if the contracts are evaluated – this must be prohibited and that’s why all methods called in contracts must be pure. Remember that Code Contracts is declarative code. It should not influence the behavior of your code, but just decorate it in some way.

Second, declaring methods as pure is generally a good thing. Beside of allowing you to use those methods in contract declarations, it furthermore helps the static checker in its task. Since method arguments can not be changed arbitrarily in pure methods, the static checker can assume that those objects will be the same after the method call.

Third (and for me that raises Code Contracts to an even higher level), declaring a method as pure can yield to a better software design and just clarifies your intent. You as programmer are able to express explicitly that your method does not have side effects. The intention of the method is revealed to callers (intention revealing), who can rely on the fact, that the state of the method’s class will be the same after calling the method as before. Thinking about declaring as many methods as possible as pure quickly brings us to command-query-separation, where you are trying to have exactly two types of methods. On the one handside the commands, which change class state and on the other handside queries, which calculate some value from current class state, but don’t modify it. Thus, queries are pure methods and with the [Pure] attribute you are able to explicitly express this intention. Dividing commands/queries and expressing queries with [Pure] is often (while not everytime) a good thing, since it leads to clear design and distinct intention and let you avoid side-effecting methods, which can be horrible code smells indeed (think of deep-nested side-effecting methods, for example).

Currently there is no component of Code Contracts which checks if methods declared pure are pure indeed. Thus if a programmer decorated a method with [Pure], it’s just believed. The Code Contracts team is working heavy on that, thus to come up with a purity checker in a future release.

(Update: thanks to AJ, I clarified my intent with the following section) Moreover one may ask: Are there any implications to automatic parallelism? The answer is: not directly. Parallelism is a hot topic and one could think, that method purity brings automatic parallelism of calls to such methods to life. And purity is indeed a strong characteristic of a method, but it’s not sufficient for the auto-par task. It’s just a one-way road, since it declares, that a method is side-effect-free (thus it doesn’t write any shared state). But in general a method can also read shared objects and depending on this it could return another value. Thus, parallelism of those method’s calls could run into problems (returning non-expected values), if the state is changed by other methods between subsequent calls. Perhaps there will be more attributes similar to [Pure] for such use cases in the future or other structures to handle that? I’m a believer…

So far for now on this topic. As you can see, decorating your methods in a declarative way with attributes like [Pure] can express your intent in a very smooth way. It helps you to clarify your design and it helps other programmers to know your intent – not just by code comments, but by checked documentation via Code Contracts.

kick it on DotNetKicks.com

Code Contracts #4: Modelling implications

Hey guys. It’s me again on Code Contracts. Sorry for not posting something on this exciting topic during the last weeks, I’ve been busy with some other tasks. This day’s post will cover some more technical ascpect of Code Contracts: how can we model implications using Code Contracts?

Code Contracts bring the DbC principle into the .NET world as one feature of the upcoming .NET framework 4.0. It’s providing statements on the code, which can be used to define specifications of how this code should work. Software elements should be understood as implementations which satisfy those specifications – that’s a very systematic approch and the core idea behind DbC. Let’s take a class method. With DbC in general and Code Contracts in particular, you’re able to define a system of obligations and benefits on this method. Obligations for clients of this method can be modelled via pre-conditions (Code Contracts: Contract.Requires(...)) to express, which conditions have to be satisfied by the client to run the method properly. In return the client get’s some benefits from the supplier (the method itself), if it maintains the obligations. Those guaranteed benefits can be defined by post-conditions on the method (Code Contracts: Contract.Ensures(...)). This obligation/benefit-based approach is very similar to contracts between humans. Example: I give you some money (my obligation as client) and you give me in return a Toyota Prius (my benefit from you as supplier), but you’re not bound to give me a Ferrari or Mercedes or something.

Thus in normal contract cases (code or real-life) you say „I give you X and you give me Y in return“. For a code example: „I give you an integer X>0 and you give me some number Y between 0 and X in return“ (e.g. a random number). But other contracts can be imagined, where the benefit depends on what has been delivered by the client. Real-world example: „I give you 40.000 $ and you give me a Toyota Prius. But if I give you 75.000 $, you give me a Mercedes S-class.“ That’s an implication. „If I give you X, you give me Y“ or shortly „X => Y. Cases can be imagined, where this could be useful in contracts on code. For example: „If you give me an empty list or null, I’ll return null. If you give me a non-empty list, I’ll return an element not equal to null.“ In this scenario, it depends if you would use a pre-condition to prohibit empty lists or null’s as parameter or not, but let’s assume those cases are normal and allowed by the method, thus shifting the responsibility to handle those in the supplier (the method) instead of the client.

Such implications are generally post-conditions on methods („I’ll give you something…“), but cannot defined directly through Code Contracts. But that’s no definite issue of Code Contracts. Implications are a special form of boolean expressions and every form of boolean expression can be used as input of a Contract.Ensures(...) call. Rather that’s a limitation of most .NET languages like C#. They don’t have an implication operator for boolean expressions and therefore don’t have direct implication support.

Solution for that is the decomposition of implications to primitive boolean expressions. Consider two boolean expressions a and b. Then the implication „a => b“ is semantically equivalent to „!a || b, which can be used in this form in any program code.

Let’s take the example from above again: „If you give me an empty list or null, I’ll return null. If you give me a non-empty list, I’ll return an element not equal to null.“ This contract can be modelled with three implications: „list==null => null“, „list.Count==0 => null“, „list.Count > 0 => !null“. Using Code Contracts and boolean substitution, we end in the following code:

public string GetSomething(IList<string> list)
{
    Contract.Ensures(!(list == null) || (Contract.Result<string>() == null));
    Contract.Ensures(!((list != null) && (list.Count == 0)) || (Contract.Result<string>() == null));
    Contract.Ensures(!((list != null) && (list.Count != 0)) || (Contract.Result<string>() != null));

    if ((list == null) || (list.Count == 0))
        return null;

    return list[0];
}

Looks a little bit frightening, doesn’t it? Moreover, the static checker will be overwhelmed with that (doesn’t have a contract on the indexer of list and thus doesn’t know, that list[0] will return a value != null). Ok, that’s perhaps not the best example, but it shows one general problem: expressions can become very big and obscure, even in relatively simple cases. That raises the question where and when to use contracts, but that’s another story…

That’s it for the moment. As you can see, implications can be used not directly, but relatively easy by use of boolean expression substitution. One could call for direct support, but that’s a language feature (providing an implication operator) and need not to be considered by the Code Contracts team. More stuff to come as soon as I find some spare time.

kick it on DotNetKicks.com

Released: Silverlight 3 Beta 1, ASP.NET MVC 1.0

Just two little quick announcements: Silverlight 3 Beta 1 and ASP.NET MVC 1.0 have been released. Here are the links:

Code Contracts #3: Contract checking

In my first two posts of this series, I covered some basic information about Code Contracts, their origins and core elements of DbC as well as the basic declarative nature of Code Contracts, the Contract Rewriter and why contracts are defined imperatively and not via attributation or additional keywords. In this blog post, I’ll dig even deeper to show the two main elements, how contracts on your code are checked…

The functionality of checking contracts/conditions on your code comes from two main components of Code Contracts: the dynamic checker (runtime checker) and the static checker. Those can be configured and activated after installation of the Code Contracts package through a new tab inside the project’s Properties window:

Configuring Code Contracts in the project's Properties windowMore information on that can be found e.g. on the Code Contracts User Manual.

The dynamic checker

The first component is the dynamic checker, which is even called runtime checker, what better implies its behavior. This type of contract checking is done at runtime of your program code. Everytime when the program execution hits a point, where contracts are defined, the Contracts runtime checks, if the contracts are fulfilled in the current context, that means with the current class state, current variable and parameter values etc. Thus the dynamic checker is searching for actual broken contracts in just the current context. Its behavior is very similar to a test (under the given context) resp. to a Debug.Assert(), leading to the term of validation of your code. If a contract check fails, then the default behavior is that a ContractException is thrown and the application terminates. This can be easily adopted to your own needs.

The static checker

So, dynamic checking ensures at runtime that no contracts are broken by current calls of your code. But it leads to the same problems as in unit testing: code coverage, choice of input/output pairs etc. Perhaps contract violations are not found during testing, because the checking with a chosen set of parameters fulfills those contracts. Problems occur, when you deliver your code and other developers use parameters that you didn’t consider and then contracts are not fulfilled any more.

The second and more interesting part of Code Contracts checking is the static checker. What’s the difference to dynamic checking? The static checker is able to check defined contracts at compile time of your code. Moreover, the static checker doesn’t only search for actual broken contracts, but for all possibilities where contracts could be broken by the defined code. For example, let’s imagine a method int Predecessor(int x), that returns the value x-1 and a post-condition on that method, that the return value is in every case ">= 0". With dynamic checking, perhaps you input some arguments for x: 1,5,100,13, … it would never lead to a situation, where the contract is broken. With static checking instead, the static checker would analyze the code at compile time and would recognize, that there are situations (every value for x < 1) where the post-condition of the method is not fulfilled. In this case, the static checker would output a warning to inform the developer of the possible contract breach.

With all this, the static checker is doing a formal verification of the defined contracts in contrast to the test-based validation of the dynamic checker. This is done by a complex algorithm that’s based on methods of formal logic and program verification and that’s why the static checker needs some time to perform the verification. The concrete algorithm is using abstract interpretation of the code, thus the code is being inspected, but not executed! By this process and with a basic rule-set on the CLR, facts about the code are generated and those facts are used to find out, if the code fulfills the defined contracts or not. The behavior of Code Contracts is very nice in comparison with the dynamic checking, but the complexity of this process may not be underestimated. Moreover, it’s heavily requiring contracts on most code pieces that you use in your contracted code, for example in the .NET framework. That’s why the Code Contracts team is currently working hard to introduce contracts all over the .NET libraries. Let’s do an example: if you have a string s and call s.Contains(), then you as programmer know that s.Contains() doesn’t change s or any other values. But if there would be no contracts on String.Contains(), then the static checker of Code Contracts could not know that Contains() is free of side effects and isn’t changing the value of s. Thus, it would warn on any post-condition of a method, that makes use of the value of s.

The following example shows a compiler warning, created by the static checker. The method WithDraw() for withdrawing money from an account has been understood and implemented as deposit (using the Deposit() method) with a negative amount. The static checker fails, because on deposit only positive values are allowed and that’s what the pre-condition on Deposit() declares. The warning is shown in the following picture. Furthermore you can see, that Code Contracts is suggesting a pre-condition on WithDraw(), by which the contract could be fulfilled.

Warning of the static checker at compile time

And that’s it again for the moment. In this blog post I’ve introduced the two core checking components of Code Contracts: the static checker and the dynamic checker. Where the dynamic checker is just doing a validation at runtime under the actual values context, the static checker is performing a complex formal verification at compile time, which finds all possible contract breaches. Those are two very different approaches and should be clear before using Code Contracts. Next blog posts will give you more examples on defining contracts and further insights.

kick it on DotNetKicks.com