Wednesday, October 05, 2011

The title of this post may generate a whole lot of questions. But that’s fine, I really don’t care. Some may think I have started some super secret project for the next propulsion system of space craft, but no, none of that is happening. It’s not hyper-ion, but just Hyperion, the name of one of the Greek mythology characters. But what has that got to do with me?

Well, I just started a little project of my own, which I decided to name Hyperion. The main objective of the program is to build a lean and mean RSS feed reader. I know, there are a million of those flying around over the Internet. But my goal is also to include many new features of the .NET 4.0 framework and have it as some sort of reference application. It’s build in C#, currently still at 3.0 version, using a WPF front-end. The application uses the M-V-VM pattern and makes use of asynchronous processing.

I also intend to include the Windows WPF Ribbon, but since the last available preview of that is not exactly what one would like and expect, that is currently on hold. Given the changes that will be made to the WPF Ribbon on the road to it’s V1 release, it would mean lot’s of double work if I were to go ahead with implementing the current version. Also, the changes that are in the pipeline will offer better support for M-V-VM, so I’ll just wait for V1 of the WPF Ribbon.

As the core feed engine, I’m using IE’s feed mechanism, so it also fully integrates with Internet Explorer, Live Mails and Outlooks capabilities of maintaining feeds. It’s just some other view on the same data, I guess. Hyperion-early alpha build The idea is to have an initial three panel view as the default, showing a tree view of the subscribed feeds, a list view of the feed items for the selected feed and a reading pane for the content of the selected feed item. It should look like the one in the picture. For the reading pane, a FlowDocument is created and provided to the panel which contains a FlowDocumentReader control.

In order to get the content of the item displayed in a well-formed manner, the HTML content is converted to XAML content of type FlowDocument. The conversion is made with the help of the HTMLToXAML conversion project floating on the web somewhere at windowsclient.com. It spells out in the readme that it is not a fully functional converter, since some tags are not supported, while others have a minimum implementation. So that’s something to work on as well. I hope I will get to that myself and at the moment consider building it using F#.

Seems like I have enough to do. So lets get working on it. Oh, BTW, one may be wondering what happened to my other over-ambitious project. The one where I was to build a Reflector like tool with support for many diagrams etc. all based on the compiled assembly code. Well, that one is still lurking somewhere, but has less priority at the moment. Besides that, it seems that integration of many features I had in mind into Visual Studio 2010 is making it more difficult for me to built something that makes VS2010 look silly. And that’s a task I’m not up to yet.

NOTE: this is a repost, I had to remove it and create it again to remove some stupid feedback item.

Meile

posted @ 2:50 PM | Feedback (6)


Monday, July 26, 2010

Like the Contract.ForAll, the Contract.Exists method comes in two flavors, one that takes two integers as lower and upper bound and a Predicate<int>, and a generic one that takes an IEnumerable<T> and a Predicate<T> as input. And where the Contract.ForAll method checks that any entry that is passed to the given Predicate returns true, the Contract.Exists method will return true if at least one of the entries returns true on the Predicate.

Let’s give a simple example. With the ForAll method  gave an example that would test a list for having the ten prime numbers greater than a given value x. It actually omitted an additional check which is the following:

      Contract.Requires(Contract.ForAll(0, primeList.Count - 1, p => primeList[p] < primeList[p + 1]));

This checks that for all items in the list, the next value is actually greater than the preceding one. In order to do something similar with the Contract.Exists method, lets write a method that requires at least one of the given numbers is prime:

    public List<int> FindAtLeastOnePrimeFollowingX(int x, List<int> numberList)
    {
      Contract.Requires(x > 0);
      Contract.Requires(numberList != null);
      Contract.Requires(numberList.Count > 5);
      Contract.Requires(Contract.ForAll(0, numberList.Count, p => numberList[p] > x));
      Contract.Requires(Contract.ForAll(0, numberList.Count - 1, p => numberList[p] < numberList[p + 1]));
      Contract.Requires(Contract.Exists(0, numberList.Count, p => numberList[p].IsPrime()));

      return (from p in numberList
              where p.IsPrime()
              select p).ToList();
    }

This is just an example showing the working of the Code Contracts methods. I have no intention to bring this as a real world example. I probably will come up which such an example in a later stage. The last precondition in the example checks the requirement that there must be at least one prime number in the list passed as the second parameter. I was going to insert a post condition in here as well, which would ensure that in the result I would also have at least one prime number, but the ensures fails with the warning:

CodeContracts: ensures unproven: Contract.Exists(Contract.Result<List<int>>(), p => p.IsPrime())

Even though the predicate on the IsPrime is in the LINQ statement, the static checker is currently not able to project this also onto the post condition that I defined. Maybe this will get better in the near future.

Next post in the series will be about the Contract.Assume method, which can be used to indicate to the static checker that even though static analysis on its own isn’t able to prove certain facts, the fact is still true and should be treated as proven.

That’s it for now
Meile

posted @ 4:08 PM | Feedback (42)


Thursday, July 22, 2010

In previous post I dabbled about the post conditions using the Contract.Ensures method. But what if the method body throws an exception? Or any called method throws? How would you ensure certain state without the Code Contracts? Probably using some try-finally construction or just a try-catch. But as with other conditions, pre and post, the try-finally and try-catch will only have impact on the current enclosing method body, and not on any derived or overridden one.

With the help of the Contract.EnsuresOnThrow<TException> this gets a little bit easier. It will ensure the post condition not only on the current enclosing method body, but also on any derived and overridden member. Let look at an example:

    public bool AddAndProcessItem(T item)
    {
      Contract.Requires(item != null);
      Contract.Ensures(this.Count == Contract.OldValue<int>(this.Count) + 1);
      Contract.EnsuresOnThrow<DbException>(!item.IsProcessed);

      try
      {
        // do processing here which may throw a DbException...
      }
      catch (DbException)
      {
        item.IsProcessed = false;
        throw;
      }

      this.innerList.Add(item);
      return true;
    }

Here the post condition ensures that on a DbExeption being thrown the item’s IsProcessed property will have the value false. The example shown here catches a possible thrown DbException, sets the state property and lets the exception propagate to a higher level. But you could also have code that throws an exception itself, for instance when a certain operation is invalid, you might throw an exception of type InvalidOperationException. If we would have the following just preceding the try-clause:

      if (this.innerList.Contains(item))
      {
        throw new InvalidOperationException("Item cannot be processed when it is already added.");
      }

we could add the following post condition:

      Contract.EnsuresOnThrow<InvalidOperationException>(item.IsProcessed == Contract.OldValue<T>(item).IsProcessed);

This would ensure that also in case of an InvalidOperationException the IsProcessed value of the item is the same as it was before entering the method. So the method body should not have ‘touched’ this property in case of the InvalidOperationException being thrown.

This concludes the parts about post conditions. In this I discussed the use of Contract.ForAll() already in this post, which is not restricted to use in post conditions, but may be used in preconditions as well. And even beyond those. There is also the Contract.Exists call, which will be the subject of the next post. After that I’ll try to post something useful on Contract.Assume and Contract.Assert. Also the object invariant is still left to discuss, with the Contract.Invariant call. And of course there are still a few attributes to dabble about.

That’s it for now
Meile

posted @ 10:17 AM | Feedback (29)


Wednesday, July 21, 2010

This post will deal with the Contract.ValueAtReturn() method of the Microsoft Code Contracts. The method enables the contract to specify post conditions on out parameters. Where the Contract.Result is used to get a peek at the final return value, the Contract.ValueAtReturn does almost the same thing on out parameters.

To make it a bit more clear, I created a simple example:

    public bool TestingOutParameter(int x, out int y)
    {
      Contract.Ensures(!Contract.Result<bool>() ?
                       Contract.ValueAtReturn<int>(out y) == -1 :
                       Contract.ValueAtReturn(out y) == x + 1);

      if (x == int.MaxValue)
      {
        y = -1;
        return false;
      }

      y = x + 1;
      return true;
    }

This tests the incoming parameter x, when it is int.MaxValue, the method will return false and y will have the value of -1, otherwise it will return true and y will equal x + 1. Please note that in the example I have included the type int in the first call, but not in the second. It would not have been necessary to put it in either call, since the compiler would have inferred the type from the usage anyway. I included it to show that it could be used in both ways. However, if the type can not be inferred, it MUST be stated and can not be omitted.

Just like the Contract.OldValue the method can only be used in a Contract.Ensures call. And speaking of post conditions, there is just one call left to deal with in that part. And that is the Contract.EnsuresOnThrow call. And that will be the subject of the next post in this series.

That’s it for now
Meile

posted @ 2:00 PM | Feedback (58)


Tuesday, July 20, 2010

Continuing our series on Code Contracts. This time with the Contract.OldValue<T>() method. This method will return the value of the given variable at the start of the enclosing method or property. It is however only valid to use this method in a post conditional Contract.Ensures method call.

And that immediately indicates it’s purpose. It should be used to enable the use of post conditions that depend on the state of the world at method entry, compared to that at the return. For instance, if you would have a class with some collection or list functionality, you could have an Add method. The Contract.OldValue<T>() method enables you to check the count at method exit compared to the count at method entry. The following example shows this:

    public void Add(T item)
    {
      Contract.Requires(item != null);
      Contract.Ensures(this.innerList.Count == Contract.OldValue<int>(this.innerList.Count) + 1);

      this.innerList.Add(item);
    }

The count at method exit should match the old count incremented with 1 for the added item. There may be other uses for the Contract.OldValue(). Just remember, it may only be used in Contract.Ensures calls, which limits the use to post conditional checking. Any other checks on pre-entry state should be handcrafted by the programmers themselves. Another way of checking object state is the use of the Contract.Invariant method calls in a private method marked with the ContractInvariantMethod attribute. A description of those will follow in some future post in this series. Next post will deal with the Contract.ValueAtReturn<T>() method call.

That’s it for now
Meile

posted @ 10:47 AM | Feedback (11)


Monday, July 19, 2010

This post in the series on Code.Contracts is all about the Contract.ForAll method. It comes in two flavors, one that iterates in a for-loop way, and a generic form that iterates over an IEnumerable of T in a more foreach kind of way.

In the example I have used so far, I included at one point the check with Contract.ForAll<char> to ensure all the characters in the result must be equal to the first character of the input string. Unfortunately the static checker of Code Contracts is unable to ensure the correctness of this for all test. It probably has got to do something with the fact that the current System.String implementation does not include the contract checks on the constructor we’re using. Hence the checker presents you with a warning like this:

CodeContracts: ensures unproven: Contract.ForAll(0, count, p => Contract.Result<string>()[p].Equals(input[0]))

I’ve tried a few things to work around this warning, but haven’t had any luck so far. So if anyone has a brilliant idea how to get rid of it, be my guest.

So I created a different example to explain the Contract.ForAll method, which will be proven nicely by the static checker. Here goes:

    public bool FirstTenPrimesFollowingX(int x, List<int> primeList)
    {
      Contract.Requires(x > 0);
      Contract.Requires(primeList != null);
      Contract.Requires(primeList.Count == 10);
      Contract.Requires(Contract.ForAll(0, primeList.Count, p => primeList[p] > x));
      Contract.Requires(Contract.ForAll<int>(primeList, p => p.IsPrime()));

      return (from p in primeList
              where !p.IsPrime()
              select p).Count() == 0;
    }

This example tests whether the list of primes in the second parameter will only contain the next ten primes greater than the value in the x input parameter. There is a number of preconditions present, all of them checking a bit of the contract. The first ensures the value of x is greater than 0, the second makes sure the list of primes is not null, the third ensures the count of the given list is 10. The fourth is a call to Contract.ForAll, this is the first flavor mentioned above. It iterates from 0 to the count of the primeList, and ensures each value is greater than x. The fifth and last check is using the second flavor of Contract.ForAll, which is the generic form. In this particular case, the type of int could have been inferred from the usage, but I’ve chosen to put it here explicitly to make it clear we’re calling the generic form of Contract.ForAll. It validates that each entry in the list is indeed prime.

Let me note that there is no real world purpose to the example’s method body. It simply confirms that there is no non-prime value in the list, which is already ensured by the method’s contract. As may have become clear from the example, the Contract.ForAll is not restricted to Contract.Ensures calls. It’s not even restricted to any Contract calls. However, be aware of how and when to use this.

The next post I will take the Contract.OldValue<T>() method as the subject. This is a method that is restricted to usage in post conditions. And there is still some ground to cover on the end of the post conditions, as there is also the Contract.ValueAtReturn<T>() method and the other post condition Contract.EnsuresOnThrow<TException> method as well.

That’s it for now
Meile

posted @ 4:59 PM | Feedback (34)

The previous post was about post conditions, and more specific the Contract.Ensures method. In the example I used another method on the Contract class, Contract.Result<T> to get the eventual result of the method. The Contract.Result<T> has been backed in to give the programmer a convenient way to get the result of the method beforehand.

The T defines the type of the return value, and logically it must match the return type of the enclosing method body. The return value of the Contract.Result<T>() method call is the actual return value of the enclosing method. The method can only be used in Contract.Ensures() method calls. So this is not some convenient way to get the return value beforehand at any place in your method body.

To refresh the memories a bit, here’s the example again:

    public string RepeatFirstCharacter(string input, int count)
    {
      Contract.Requires<ArgumentNullException>(input != null);
      Contract.Requires<ArgumentException>(input.Length >= 0, "The input should have at least one character.");
      Contract.Requires<ArgumentOutOfRangeException>(count > 0);
      Contract.Requires((0 + 1) <= input.Length);
      Contract.Ensures(Contract.Result<string>().Length == count);

      return new string(input.ToCharArray(0, 1)[0], count);
    }

The Contract.Ensures call now verifies that the return value of the enclosing method has actually got a length that is equal to the count input parameter’s value. I’ve also added another precondition, since the static code checker of Code Contracts proposed another precondition, to ensure the result can be correctly computed. It’s the following line:

      Contract.Requires((0 + 1) <= input.Length);

This ensures the result can use the ToCharArray(0, 1) code without a possible exception being thrown at you at runtime. In my last post I also referred to the Contract.ForAll<T> method. This will actually be the subject of the next post in this series.

That’s it for now
Meile

posted @ 9:55 AM | Feedback (39)


Thursday, July 15, 2010

This is the first post that will be about post conditions. So far, I’ve tried to shred some light on defining preconditions with the help of the Code Contracts that are now part of the .NET framework since version 4. In the past, preconditions could and would be defined with the help of the IF-THEN-THROW construction. For a broader explanation on that, see my previous post in this series.

Now I’ll move on to post conditions. I have not often included post conditions in my code. Of course you would design your code to never return a null value, of that would be a requirement. But how would you go about checking that? A possible construction would be the following:

    public int Process()
    {
      var processable = from p in this.currentList
                        where p.Processable
                        select p;

      int result = processable.Count();

      // process the bunch....

      if (result != processable.Count())
      {
        throw new Exception("Count does not match number of processed items");
      }

      return result;
    }

The code above has some points to be cautious about. For instance, the value in the variable that is returned might have been changed on a different thread, before it is returned by the method body. How would you verify that? That would not be easy, especially not when your code is not as succinct as it could be and probably has dependencies you were not even aware of. Of course the code above contains a major flaw, since it uses a LINQ query to determine the count of items. But would every developer be aware of this?

Luckily now there is the Contract.Ensures method to the rescue. As I’ve stated before, there is no ‘silver bullet’, and this one is no exception. It does not end all bugs in your code, but it goes a long way. The binary rewriter would make sure the code is checked at the end of the method. But that’s something you could implement yourself. However, the static checker goes the other mile, by checking what you’ve stated must be true. And in the above example, if it were written with the use of Contract.Ensures, the checker would warn you about the fact that the currentList’s entries may have their Processable property changed and therefore it can not verify the correctness of your post condition.

Now back to our main example targeted also in our previous posts. Rewritten with the help of the Contract.Ensures method it will become like this:

    public string RepeatFirstCharacter(string input, int count)
    {
      Contract.Requires<ArgumentNullException>(input != null);
      Contract.Requires<ArgumentException>(input.Length >= 0, "The input should have at least one character.");
      Contract.Requires<ArgumentOutOfRangeException>(count > 0);
      Contract.Ensures(Contract.Result<string>().Length == count);

      return new string(input.ToCharArray(0, 1)[0], count);
    }

This verifies that the length of the returned string value is equal to the int count parameter. An additional check could be the following:

      Contract.Ensures(Contract.ForAll<char>(Contract.Result<string>().ToCharArray(), p => p == input[0]));

This verifies that result only contains the first character of the string input parameter. You may have been wondering what this construction Contract.Result<> is used for. Well, that will be the topic of the next post in this series. And the Contract.ForAll<> will follow in another post as well. Just stay tuned.

That’s it for now.
Meile

posted @ 3:44 PM | Feedback (51)


Tuesday, July 13, 2010

In this post of the series on Code Contracts, it’s all about the Contract.EndContractBlock method. This method could be seen as some magical marker to get the benefits of Code Contracts and all the checks that come with them. It is intended to be used in legacy code to mark the end of a contract block.

Given the example I used in my previous posts:

    public string RepeatFirstCharacter(string input, int count)
    {
      if (input == null)
      {
        throw new ArgumentNullException("input");
      }

      if (input.Length < 1)
      {
        throw new ArgumentException("The input should have at least one character.", "input");
      }

      if (count <= 0)
      {
        throw new ArgumentOutOfRangeException("count");
      }

      return new string(input.ToCharArray(0, 1)[0], count);
    }

This could very easy be rewritten with a call to the Contract.EndContractBlock() method to get the benefit of the Code Contracts. It would end up like this:

    public string RepeatFirstCharacter(string input, int count)
    {
      if (input == null)
      {
        throw new ArgumentNullException("input");
      }

      if (input.Length < 1)
      {
        throw new ArgumentException("The input should have at least one character.", "input");
      }

      if (count <= 0)
      {
        throw new ArgumentOutOfRangeException("count");
      }

      Contract.EndContractBlock();

      return new string(input.ToCharArray(0, 1)[0], count);
    }

There are some things to note here though. Not every block of argument checking etc. could be easily marked with the EndContractBlock call. Any code that precedes the call to Contract.EndContractBlock() must adhere to the following form:

if throw

There can not be an else branch in the statements. Also the code in the condition must be side-effect free, and the exception that is to be thrown must be at least as visible as the method in which the contract occurs. As mentioned already in my post on Contract.Requires, the conditions in the IF-THEN-THROW statements are the negation of the conditions that occur as part of the Contract.Requires method. This is something to be aware of when working with contracts.

The Code Contracts binary rewriter will convert the code marked by the Contract.EndContractBlock into code similar to the code that uses Contract.Requires which was explained in my previous post here. The Contract.EndContractBlock call is only needed as a marker when there are no other or further calls to the Contract’s static members. If we were to enhance the code with an additional precondition, or with a new post condition, it would make the call to Contract.EndContractBlock() obsolete.

The following example would also result in use of all benefits of Code Contracts, even though there is no explicit call to Contract.EndContractBlock():

    public string RepeatFirstCharacter(string input, int count)
    {
      if (input == null)
      {
        throw new ArgumentNullException("input");
      }

      if (input.Length < 1)
      {
        throw new ArgumentException("The input should have at least one character.", "input");
      }

      if (count <= 0)
      {
        throw new ArgumentOutOfRangeException("count");
      }

      Contract.Ensures(Contract.Result<string>().Length == count);

      return new string(input.ToCharArray(0, 1)[0], count);
    }

This example has a new post condition that has been added. The call to Contract.Ensures is a post conditional check, which is performed on the result of the method. Contract.Ensures is to be explained in the next post in this series.

That’s it for now.
Meile

posted @ 2:45 PM | Feedback (50)


Monday, July 12, 2010

The previous post on Code Contracts was about Contract.Requires. That method comes with an overload, which is a generic one that takes an Exception type as the generic type parameter. The purpose of this method is mainly in line with that of the Contract.Requires method that I explained in the previous post here.

The original code sample contained a few ArgumentExceptions that were thrown if certain conditions were not met. The use of the Contract.Requires method made the code more succinct with less clutter, but the exceptions were nowhere to be found. In case the precondition is not met in the code that uses Contract.Requires, a ContractException will be thrown at runtime. Sometimes it is feasible though to throw a more specific exception, like the ArgumentExceptions that were thrown in the IF-THEN-THROW constructions.

Just to step back to the code we had initially:

    public string RepeatFirstCharacter(string input, int count)
    {
      if (input == null)
      {
        throw new ArgumentNullException("input");
      }

      if (input.Length < 1)
      {
        throw new ArgumentException("The input should have at least one character.", "input");
      }

      if (count <= 0)
      {
        throw new ArgumentOutOfRangeException("count");
      }

      return new string(input.ToCharArray(0, 1)[0], count);
    }

This code is very specific about the exceptions. About the ArgumentOutOfRangeException one could argue that it is actually not a correct exception to throw here, since there is no specific range, but beyond that, the exceptions serve a purpose. It is up to the requirements of the final code and build whether or not the exception must be of the  ArgumentException family, or it should be a more ‘general’ ContractException, since it involves the predefined contract. When it is necessary to have the existing exceptions, one should use the Contract.Requires<TException> overload. The example code would end up looking like this:

    public string RepeatFirstCharacter(string input, int count)
    {
      Contract.Requires<ArgumentNullException>(input != null);
      Contract.Requires<ArgumentException>(input.Length >= 0, "The input should have at least one character.");
      Contract.Requires<ArgumentOutOfRangeException>(count > 0);

      return new string(input.ToCharArray(0, 1)[0], count);
    }

Beyond the fact that the more specific exception is used on contract failure, all other points mentioned in the post on Contract.Requires, also apply to Contract.Requires<TException>. The overload has an additional caveat though. The exception type that is to be thrown must have a public constructor accepting a single string argument. If such a constructor can not be determined at runtime, an internal ContractException will be created and thrown instead.

To conclude the posts on preconditions, the next will handle about Contract.EndContractBlock(). Even though it is not specific for preconditions, it will only truly serve a purpose when it appears at the end of legacy preconditions that are stated in the form of IF-THEN-THROW.

That’s it for now.
Meile

posted @ 9:38 PM | Feedback (22)

This second post in the series on Code Contracts will deal with the Contract.Requires method. In the introduction, I already mentioned that the Contract.Requires method is used to express a precondition. Whenever something has to be validated upfront, the Contract.Requires method is the one to use.

In the old style programming, any precondition would be stated as an IF-THEN-THROW construction, like in the following example:

    public string RepeatFirstCharacter(string input, int count)
    {
      if (input == null)
      {
        throw new ArgumentNullException("input");
      }

      if (input.Length < 1)
      {
        throw new ArgumentException("The input should have at least one character.", "input");
      }

      if (count <= 0)
      {
        throw new ArgumentOutOfRangeException("count");
      }

      return new string(input.ToCharArray(0, 1)[0], count);
    }

Not only does this create a lot of clutter, it also expresses the conditions from the negative, exceptional point of view. Looking at the code, it is required for the input to be a non-null string with a length of 1 or more. But the conditional check is on a null string value, and a length smaller than 1. If we were to rewrite the code above with the use of Contract.Requires, we would end up with the following code:

    public string RepeatFirstCharacter(string input, int count)
    {
      Contract.Requires(input != null);
      Contract.Requires(input.Length >= 0);
      Contract.Requires(count > 0);

      return new string(input.ToCharArray(0, 1)[0], count);
    }

Now all the clutter has gone. The code is more succinct, and the conditions really reflect the contract in  a non-exceptional manner. Given the fact that in many software development cycles the specifications are mainly written in terms of requirements, it’s a good thing to have this also in the code. Since the Code Contract preconditions, post conditions, object invariants etc. can all be merged into the generated XML documentation, this also means the requirements will also appear in them as well.

Moreover, the contracts as defined using the IF-THEN-THROW style will only affect the current call. If the RepeatFirstCharacter method had been defined as a virtual method, any derived class that implements an override will have to check for the contract itself. When using Code Contracts, this is no longer necessary. The binary rewriter used by Code Contracts will make sure the contract is also exposed in the derived method as well as in the base method.

All this comes with a few caveats though. Besides the fact that Contract.Requires calls must be at the beginning of the method (which is quite logical given their nature), the contract must only reference members with at least the same visibility as the enclosing method. Since the contract is exposed to clients calling the method, this requirement makes a lot of sense. Another caveat is that on a derived method additional requirements can not be set. This is one that also makes a lot of sense, since the interface definition largely determines the contract. And on an override, the interface isn’t changed, so why should the contract?

This method should be used for those preconditions that do not enforce a particular exception to be thrown, e.g. for backward compatibility reasons. In case a particular exception should be thrown one would have to use Contract.Requires<TException>(Boolean) method instead. I will dig into that method in the next post in this series.

That’s it for now.
Meile

posted @ 10:28 AM | Feedback (11)


Friday, July 09, 2010

This is the kick-off for my series on Code Contracts, a new addition to the .NET framework, built-in from version 4 and back ported to .NET 3.5 by use of the Microsoft.Contracts assembly. In this first post I’ll try to give a general introduction to the Code Contracts. Just what is it and what purpose does it serve.

I guess many developers have had there time writing classes for some wanna-be framework and trying to defend themselves against all kind of bogus input. So on method entry all parameters are checked for non-null values, for proper values within a predefined range, etc. Throwing ArgumentExceptions and ArgumentNullExceptions all around. An occasional ArgumentOutOfRangeException might also be on the list. And you might conclude you have your method sealed and locked down. No further hassling with the parameters, everything works perfect.

But what about the callers of your locked-down method? Are they going to obey your contract? Or are they just going to put the whole thing in a try-catch bloc and catch the ArgumentExceptions? Which IMHO is always wrong, but that’s a different issue. The compiler won’t complain about a null being passed, even though the method that is called will check for it and throw an ArgumentNullException. It will only appear as such at runtime. And this sums up just two issues we face today when designing and implementing validation checks on method entry.

Just come to think of it, what happens when your precious method gets overloaded in a derived class? You could argue that such a thing should not be possible in a valid interface design and inheritance should be on some protected method and not on a private one. But still, there is no way you can enforce your ‘contract’ to the derived method. It is not obligated to call the base method, and even if it would, it is not ensured that it would happen directly on entry of the method body. Sometimes that would even be the complete opposite of the desired way of coding.

So what’s next? There is no ‘silver-bullet’. Not for parallelism in coding, but also not for ensuring a public contract on a method. But now there is Code Contracts from Microsoft. It’s not the definite answer, but it comes a long way. The issues I mentioned above about runtime failure, inheritance and such do not apply to Code Contracts. Code Contracts get inherited by derived classes and overridden methods. And since the Code Contracts can be statically checked during compile time, it will help developers to deliver better code, with fewer runtime failures.

But what is Code Contracts? As defined at the Microsoft site:

“Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs. The contracts take the form of preconditions, post conditions, and object invariants. Contracts act as checked documentation of your external and internal APIs. The contracts are used to improve testing via runtime checking, enable static contract verification, and documentation generation.”

I could not come up with a better phrase. As can be read from this definition, the Code Contracts take the form of preconditions, post conditions and object invariants.

The following gives a quick overview of each of these:

  • Preconditions
    The preconditions define the state of the world at method entry. They must be true to ensure successful execution of the method. Often you’ll find yourself using preconditions for parameter validation. It is however still the responsibility of the caller to make sure the conditions are met. The preconditions comes in three flavors with Code Contracts:
    • Contract.Requires
      This method states a precondition, simple, plain. A small example:

      Contract
      .Requires(root != null);
    • Contract.Requires
      This method also states a precondition, but adds to the previous call a throw of the specified exception. It is also always included in the final code, as opposed to some other calls on Contract.  Here’s an example:

      Contract
      .Requires<ArgumentNullException>(root != null);
    • Contract.EndContractBlock()
      This method is to be used in legacy code where the preconditions are defined in the common way of ‘IF [condition] THEN throw [exception]’. Take for example the following code:

      if
      (root == null)
      {
        throw new ArgumentNullException("root");
      }

      Since it would not be feasible to go through all your code and rewrite all IF-THEN-THROW sections into Contract.Requires calls, the Contract.EndContractBlock method is a way of telling the tools that any preceding code in the method body before this call must be considered as preconditions. So the example should be changed to:

      if
      (root == null)
      {
        throw new ArgumentNullException("root");
      }
      Contract.EndContractBlock();

      This is needed only when there are no other contracts in the code. If you would add a post condition, the code would look like this:

      if
      (root == null)
      {
        throw new ArgumentNullException("root");
      }
      Contract.Ensures(this.currentRoot != null);
  • Postconditions
    Post conditions give a guarantee on the state at method exit. So what must be true in the state of the world when the method returns control to it’s caller. These conditions are the responsibility of the method. The declaration of the post conditions is set at the beginning of the method, just like the preconditions. The tools that come with Code Contracts will hustle the code and make sure they get called at the right times. This type of condition comes in two flavors:
    • Contract.Ensures
      This method states that a condition must be true on successful method exit. A possible example would be, upon leaving a Save method for instance:

      Contract.Ensures(this.Name != null);
    • Contract.EnsuresOnThrow
      This method enables validation of conditions at unsuccessful method exit. When the method is faced with exceptional termination, post conditions can be met for the specified exception type. A word of caution is at place here though. It is generally not a good idea to make assumptions for all exception types, so letting TException be Exception is just plain foolish. One cannot guarantee anything on the state of the world when for example a StackOverflowException or an OutOfMemoryException is thrown. Some exceptions that may be more appropriate in this case could be IOException or DbException, like so:

      Contract
      .EnsuresOnThrow<DbException>(this.Name != null);
  • Object Invariants
    The last form of Code Contracts mentioned is Object Invariants. These statements define what must be true at all public method exits for an object (instance). The responsibility of maintaining the object’s invariant is up to the developer. Object invariants must be contained in a separate method that is to be marked with the ContractInvariantMethodAttribute attribute. The name of the method is not important, but it’s signature must be a parameter-less method with a void return type. The method body must only contain calls to the Contract.Invariant(…) method, of which there must be at least one. The following example defines an invariant which states that the value in the field is never null:
    [ContractInvariantMethod()]
    void ObjectInvariant()
    {
      Contract.Invariant(this.propertyNameToHandlerMap != null);
      Contract.Invariant(this.propertySourceReference != null);
    }

In the following posts in this series I plan to be more specific on each of the mentioned methods. For now, I’ll leave it to this, with some useful links to conclude with:

That’s it for now
Meile

posted @ 5:27 PM | Feedback (17)

I need your help. I have entered a contest on the LessThanDot forums to get a shot at an MSDN Ultimate subscription. Now all that is left is a vote for the one remaining subscription. So who's with me and willing to vote for me? Head over to http://forum.lessthandot.com/viewtopic.php?f=121&t=11550 and vote for me!

Hurry, the clock is ticking....

That's it for now.
Meile

posted @ 3:46 PM | Feedback (2)


Saturday, July 03, 2010

Once again I managed to get the full load of .NET 4 certifications. I passed on all 6 exams, which I took in the BETA program. It makes me wonder how many .NET 4 certified people there are in my country, The Netherlands, but also how many there are all over the world. In the past there used to be a page within the Microsoft Learning site, which showed the numbers of certified people worldwide. But this page can no longer be found. At least I tried to track it down, but with no luck so far.

Now I have these certificates, I think it is ‘payback time’. I’ve tinkered with the idea to do a series of posts on the Code Contracts that can be found in the new .NET framework. And possibly followed by a series on Rx, Reactive Extensions for .NET. Both technologies have gotten me really excited about .NET 4 and the many things that are hopefully still to come from MSFT. And given the recent announcement of IIS Express by Scott Guthrie, that will most likely be no problem for many years to come.

The series on Code Contracts will probably have a setup where each post will have details on a specific member of the System.Diagnostics.Contracts.Contract class. Also the attributes in the System.Diagnostics.Contracts namespace will probably have a post of their own. And starting the series with a more general post and concluding with a final wrap-up. So, many things to do in the coming months.

That’s it for now
Meile

posted @ 2:18 PM | Feedback (3)


Thursday, March 04, 2010

I have been going a while without the Adobe Flash player installed on my machine. I mainly chose to do this, since I think Flash hurts my machine in many ways. For starters it’s one of those memory hogs that just keeps sucking memory, and leaving me to the will of the Flash programmer who may or may not have figured out to give me the claimed memory back. I also came across a page on the net that gives me 7 Reasons to Stop Using Flash.

And beyond that there are the security issues. It’s something which I thought of already in the light of all the recent attacks on Internet Explorer etc. And my opinion on the matter was further influenced by the fact that someone like Steve Jobs said that Flash is not secure. And just a few days ago I read this article on Neowin citing Charlie Miller, who literally said: ‘The main thing is not to install Flash!’. This all in the light of possible attack surfaces on a PC.

So, this is where my crusade against Flash starts. I think we will see many more people abandoning Flash, since in the near future there will be HTML5 which will also have many aspects that will make Flash less necessary for any web development in the need of media rich content. And also there is Silverlight, Microsoft's take on delivering rich internet content. So abandon Flash now!

Who’s with me on this one?

Since the web won’t change from full of Flash to a lot less Flash overnight, I have forced myself to use a virtual machine any time I need to get to some Flash content. And that’s only when there is definitely the need to see the Flash content. Otherwise I’ll just ignore it completely.

So, once more, who’s with me on this one?
Meile

posted @ 2:36 PM | Feedback (4)


posts - 24, comments - 286, trackbacks - 0, articles - 0

Copyright © Meile Zetstra