Code Contracts and form controls

I'm trying to get a grip on Code Contracts as I think the concept holds great promise in regards to producing more robust code, but so far quite a few things are still unclear to me or seem cumbersome.

One of the biggest questions I currently have is how to correctly handle form controls. With "Implicit Non-Null Obligations" selected in the static checking options, I get a message开发者_运维问答 recommending a Contract.Requires([control] != null) rule for each and every control within the current form which I access; this is a little pointless because I know the controls will always be there as they are created in the form's InitializeComponent() method.

I know the static checker cannot know about that, but there has to be a way of getting rid of those messages (if only because they clutter up the list) - at least I hope so - other than the obvious adding all those recommended checks (or maybe rather Contract.Assume() calls), which would then clutter up my code while being effectively (logically) redundant.

What is the correct way to deal with this ? Adding invariant rules for all the controls requiring them to always be non-null ? And what about the object members that I know will always be there, like ComboBox.Items ?

Thanks for sharing any insights on this.

---

The simplest way to deal with it is to add object invariants like this:

[ContractInvariantMethod]
private void Invariants()
{
    Contract.Invariant(control1 != null);
    Contract.Invariant(control2 != null);
    // etc
}

I think you'll also need to Assume that these are not-null after the InitializeComponent call, since Code Contracts doesn't know what happens inside that (this is needed for Code Contracts to prove that the Invariants hold by the end of the constructor).

Once you've done that, the static checker will know that these invariants hold (i.e. the controls are not-null) at the end of the constructor, and that they will always be not-null in any other methods.

For other things like ComboBox.Items, you'll have to Assume for now, since they don't have contracts in the BCL. You can request for contracts to be added in this thread on the Code Contracts forum.