Code Contracts Static Checker: Best practices & guidelines

This blog has moved, you should read this at my new place www.koenmetsu.com!

As stated previously, Code Contracts can give you certainty that your classes behave exactly in the way you want them to.
By defining pre- and postconditions on them, you can tell what you expect from a certain class and what others can expect from your classes.

A number of posts and concerns about Code Contracts revolve around the static checker, and how to make it prove that certain contracts are correctly followed.
Sometimes this can be quite challenging, though I see this more as a pro than a con.
Making you think twice (or more) about your code is never a bad thing, really.

But for those who desperately seek salvation in their quest to annihilate all static checker warnings ( with or without Contract.Assume() ), I would recommend the following guidelines:

1. Install the Code Contracts Extension for Visual Studio 2010.
2. Use Reflector to see Code Contracts on the Base Class Libraries.
3. Use Pex to automatically test your methods.
4. Split more complicated statements into multiple lines.

1. Code Contracts Intellisense.

Install the Code Contracts Extension for Visual Studio 2010. This brings contracts right to your Intellisense as you type, as well as some other handy features.

2. Use Reflector to see Code Contracts on the Base Class Libraries.

When you use the static checker, you might notice that a lot of methods in the BCL already have contracts defined on them. For example, the IList.Clear() method has a postcondition stating that the Count property will be equal to zero.

These contracts are not magically inferred from the BCL assemblies, but rather found in the Contract Reference Assemblies that are included with the Code Contracts installation. These assemblies are found under <%YourProgramFiles%>\Microsoft\Contracts\Contracts\.NETFramework\v4.0.

Code Contracts BCL Assemblies

Code Contracts BCL Assemblies

Using Reflector you can browse through these assemblies, which contain nothing but Contracts. Although a lot of methods already have contract defined on them, the BCL contract assemblies still have a lot of contracts missing.
Using Reflector on these assemblies, you can find out for yourself why you keep getting a warning that a certain “contract cannot be proven”.

Code Contracts String.Format in Reflector

Code Contracts String.Format in Reflector

3. Use Pex to automatically test your methods

Pex provides a way to create parameterized unit tests to see which input causes your method to violate a contract. Actually, it does a lot more than that. Way too much to elaborate on in this post.

To make a long story short, Pex can automatically unit test your parameterized methods with different kind of inputs ( without resorting to brute-force). What’s great about this, is that it works in combination with Code Contracts, and can actually suggest contracts for you.

The documentation pages includes a nice tutorial on how to use the power of Pex in combination with Code Contracts.

4. Split more complicated statements into multiple lines.

Although simple, quite effective.

A lot of concerns surrounding the static checker’s inability to prove something are easily solved by this one. Some developers have the tendency of joining multiple statements in one big statement. This can improve readability and shorten your code files, but also confuse you about which statement the static checker is complaining about.

Split your big statement into several lines, and it will become more clear which method the static checker is complaining about.

For example:

StringHelper.CleanUrl( new PageManager(“BasePage.aspx”).GetFullUrl()) ;

has a lot of places where there could be a nullreference occurring. Splitting this into several statements would make this a lot easier for you to see what method gives you the problem. ( This is actually general debugging advice, not just for the static checker )

Conclusion

A lot of static checker warnings will easily be solved by following one or more of the solutions provided here, others will require more digging through your own code. There will be times when you will still need to Assume some conditions, as the static checker will never be able to statistically proof every line of code you write.

However, hopefully these guidelines will aid you in proving your contracts to the static checker, further improving your code base with better documented behavior, promises and expectations.

Advertisements

New Code Contracts Extension: See Contracts in Intellisense

This blog has moved, you should read this at my new place www.koenmetsu.com!

Code Contracts just got a whole lot better with a brand new extension for Visual Studio 2010!

This new extension brings a couple of cool new features that help you while developing with Code Contracts.

See contracts as you type

Just start typing a method with contracts, and they will be listed right beneath the description of the method.

The great thing about this is that it works for methods in the BCL as well as your own methods.

See inherited contracts

Contracts that are inherited show up above your methods. It’s a helpful visual reminder of the contracts that are defined on the interface or class you’re inheriting from.

This way you can easily add preconditions and postconditions without having to look back and forth to see which contracts are already defined.

And it doesn’t actually add text to your code file, it’s just an adornment which you can easily click away too.

See contracts for external assemblies

Another helpful addition is being able to see contracts of external assemblies. The contracts are visible in the metadata file you see when you ‘go to definition’ of a member of a class of which you don’t have the source.

This can also be disabled by a simple click of a button labeled “Hide all contracts” ( See, it’s all obvious ).

Conclusion

Before this extension, visibility of the contracts was one of my major concerns with Code Contracts. Not being able to see contracts as you type made you rely on the static checker to see what contracts were defined on your code. This extension is a great improvement and incentive to using Code Contracts. It’s only just released, but I’m loving it already!

Great! So how can you have a piece of this?

It’s easy!

  1. Install the latest version of Code Contracts
  2. Install the Code Contracts Editor Extension for Visual Studio 2010.
  3. Enable Code Contracts and choose ‘Build’ for ‘Contract Reference assembly’ in the Code Contracts properties pane.
  4. Build your code

And you’re ready to see your contracts showing up as you type! Have fun =)

Code Contracts: Is the static checker really that thick?

This blog has moved, you should read this at my new place www.koenmetsu.com!

When you start working with Code Contracts, you often get the feeling that you have to add contracts everywhere for everything. When you enable the static checker on an existing project, you might get a lot of warnings.

A lot of these

A lot of these

Something that troubles starting users is the fact that you have to add a lot of contracts ‘twice or more’. I’ve recently seen this issue appear on stackoverflow as well. You can check out the specific code sample there, but I’ll lay it out for you here as well. Suppose you have a public method calling a private method, both of which accept an input parameter of type string.

public void ValidateString(string givenString)
{
    Contract.Requires(!string.IsNullOrEmpty(givenString));

    var isValid = SomeValidatingMechanism( givenString );
}

private bool SomeValidatingMechanism( string toValidate )
{
    return toValidate.Contains("someImportantValue");
}

I’ve immediately added a precondition to the ValidateString method, to make sure the caller never wrongfully provides me with an empty string and make my application crash to death.

Now when you let the static checker loose ( and you’ve set it to check for possible nullreference occurrences), it will whine about my private method calling Contains on a possible null value. What’s that all about? I added a precondition to the public method, so the toValidate string can’t be empty, right?

Solution

Well, actually the static checker is really thinking ahead here.

First of all you’ve got the static checker which cannot prove that the the toValidate string isn’t actually null. You know it, because you can clearly see from the code above. But the static checker cannot mathematically prove that you did not alter the toValidate string after it entered the public method. For all it knows, you might have maliciously set it to be null right after it entered the method, trying to crash my application once again! This might seem like a limitation to the static checker, but imagine you made some calls to an external API before you called the private method here. The static checker is just really playing it safe.

Secondly, for now you might have only one call to the private method, but what happens when you add more calls to it from methods which didn’t have a precondition like the one above? Adding a precondition to the private method now can prevent future errors and possibly lots of debugging.

public void ValidateString(string givenString)
{
    Contract.Requires(!string.IsNullOrEmpty(givenString));

    var isValid = SomeValidatingMechanism( givenString );
}

private bool SomeValidatingMechanism( string toValidate )
{
    Contract.Requires(!string.IsNullOrEmpty(toValidate));
    return toValidate.Contains("someImportantValue");
}

With the above code the static checker’s warning is gone, and your code feels safer once again =) You can sleep tight and never worry about some co-developer calling your private method with an empty string.

So no, the static checker isn’t really that thick, it’s actually quite smart and following it’s advice can often lead to better and safer code.

Using Code Contracts to define behavior

This blog has moved, you should read this at my new place www.koenmetsu.com!

First: an introduction

Code Contracts is a language-agnostic tool that provides you the power of Design By Contract development. In short, it enables you to make statements about what your code expects and delivers. It’s a great way of telling whether or not your code does what you expect it to do.

Actions speak louder than words, so let’s bring in an example: the BankAccount class.

public class BankAccount
{
public decimal Balance { get; set; }
public double InterestRate { get; set; }

public void Withdraw(decimal amount)
{
Balance -= amount;
}

public void Deposit(decimal amount)
{
Balance += amount;
}

public void AddInterests()
{
var interests = Balance * (decimal)InterestRate;
Balance += interests;
}
}

A real simple class that should speak for itself. It maybe could use some comments, DDD or better logic, but it’ll do for this post.

Adding preconditions

Preconditions are a way to define what state your application must be in at the start of execution of a called method. They’re all about telling what you expect from someone calling your methods.

Let’s take the Withdraw method: someone withdraws money from their account. We might have the following expectations:

  • If you withdraw money, you should at least have money on your account.
  • You have to withdraw some money, which means more than nothing ( else it wouldn’t be really withdrawing, would it? ).
  • You aren’t allowed to withdraw more money than you have.


All of these expectations can easily be converted to preconditions in Code Contracts, by using the Contract.Requires method.

public void Withdraw(decimal amount)
{
Contract.Requires(amount > 0);
Contract.Requires(Balance > 0);
Contract.Requires(Balance >= amount);
Balance -= amount;
}

The nice stuff is that you’re not only defining the state your application must be in, you’re also defining behavior here.

Adding postconditions

Postconditions define what state your application should be when it leaves the called method. This is the part that’s all about delivering promises about your code, as well as checking if the method did what you expected it to do.

For the Withdraw method:

  • We state that after we withdraw money, the balance of the bank account won’t be negative.
  • We also state that after the withdrawal, the balance will be the starting balance ( when we entered the method ) minus the amount we withdrawn.


Once again, the postconditions are easily converted to contracts. The Contract.OldValue() represents the value of a certain field or parameter as they were in the beginning of the method.

public void Withdraw(decimal amount)
{
Contract.Requires(amount > 0);
Contract.Requires(Balance > 0);
Contract.Requires(Balance >= amount);
Contract.Ensures(Balance == Contract.OldValue(Balance) - amount);
Contract.Ensures(Balance >= 0);

Balance -= amount;
}

The second statement here seems pretty obvious because of the actual code following the contracts, but a lot of times this code will obviously be quite more complicated.

Isolating object invariants

Object invariants are conditions on an object which should be true at all times that object is visible to a client. They express the conditions under which the object is in a “good” state.

As good programmers we try to prevent writing the same code twice, and if we look at the preceded code we notice the balance must always be greater than zero.

For the balance to be in a good state, it must never be zero.

We can isolate this contract by creating a method that contains Contract.Invariant() statements, and decorate this method with the ContractInvariant attribute.

[ContractInvariantMethod]
private void EnsureBalanceIsPositive()
{
Contract.Invariant(Balance > 0);
}

All the invariants will be checked at the end of every public method. So now we added these, we no longer need the preconditions regarding the balance being greater than zero.

Conclusion

Although this example uses really simple code, by using Code Contracts we made it exactly clear what this BankAccount can and cannot do.

Your code can become immensely more complicated, new developers can join your project but by defining the behavior of this class by contracts, they will immediately recognize what the class does.

Ideally we would define the contracts on an interface or base class, so deriving classes would all share a base behavior, but that’s out of scope for this post. =)

For more info on Code Contracts, visit the homepage here.