Why am I getting malformed contract, in by C# code?

Question

Visual Studio shows an error when I write this contract below.

Error 20 Malformed contract section in method '....get_Page'

Is the problem with the if block?

public int? Page
{
  get
  {
    int? result = Contract.Result<int?>();

    if (result != null)
        Contract.Ensures(result >= 0);

    return default(int?);
  }
}

EDIT:

Lasse V. Karisen has posted in comments:

How about: Contract.Ensures(result == null || result >= 0); ?

Yes Karisen, I've tried this before and it compiles. But the question remains: isn't it possible to have ifs when using contracts?

Another problem I'm having is clueless (mainly considering the example above works), involves the use of result also:

public int IndexOf(T item)
{
    Contract.Assert(item != null);
    Contract.Assert((item as IEntity).ID > 0);

    int result = Contract.Result<int>();
    Contract.Ensures(result >= -1);

    return default(int);
}

Answer 1

Just having a guess. Perhaps it should be Contract.Ensures(result.Value >= 0)?

Answer 2

The contract is malformed because all contract clauses MUST appear before any other code.

Answer 3

You do not need an if, to do boolian manipulation instead use implies!

public int? Page
{
    get
    {
        Contract.Ensures( (result!= null).Implies(result >= 0) );
        var result = ...

        ...


        return result;
    }
}

Also you should use Requires not assert when testing method arguments, and other preconditions.

public int IndexOf(T item)
{
    Contract.Requires(item != null);
    Contract.Requires((item as IEntity).ID > 0);
...

Answer 4

All Ensures and Requires calls must be before all other statements in a method or property body, this includes simple assignments like you're using that help readability.

Proper syntax

public int? Page {
    get {
        Contract.Ensures(Contract.Result<int?>() == null 
            || Contract.Result<int?>() >= 0); 

        return default(int?);
        }
    }
 }

This is very ugly, much uglier than normal if (x || y) throw new ArgumentOutOfRangeException().

Special Attributes

There is a somewhat roundabout way of getting around this. ContractAbbreviatorAttribute and ContractArgumentValidatorAttribute are special attributes that the ccrewrite understands which make your life easier. (For lots of details see the System.Diagnostics.Contracts namespace documentation on MSDN or the Code Contracts manual.)

If using .NET 4 or older: These attributes are in the framework starting .NET 4.5, but for prior versions you can get a source file for them from the directory Code Contracts installs to. (C:\Program Files (x86)\Microsoft\Contracts\Languages\) In that folder are CSharp and VisualBasic subfolders that have a ContractExtensions.cs (or .vb) file containing the required code.

ContractAbbreviatorAttribute This attribute effectively lets you create contract macros. With it, your page property could be written like this:

public int? Page {
    get {
        EnsuresNullOrPositive();
        return default(int?)
    }
}

[ContractAbbreviator]
static void EnsuresNullOrPositive(int? x) {
    Contract.Ensures(
        Contract.Result<int?>() == null ||                 
        Contract.Result<int?>() >= 0);
}

EnsuresNullOrPositive could also be kept in a static class and reused across your project, or made public and placed in a utility library. You could also make it more general like the next example.

[ContractAbbreviator]
static void EnsuresNullOrPositive<Nullable<T>>(Nullable<T> obj) {
    Contract.Ensures(
        Contract.Result<Nullable<T>>() == null ||                 
        Contract.Result<Nullable<T>>() >= default(T));
}

For my own utility library, I have a static class named Requires and a static class named Ensures, each with many static methods decorated with ContractAbbreviator. Here are some examples:

public static class Requires {

    [ContractAbbreviator] 
    public static void NotNull(object obj) {  
        Contract.Requires<ArgumentNullException>(obj != null);
    }

    [ContractAbbreviator]
    public static void NotNullOrEmpty(string str) {
        Contract.Requires<ArgumentNullException>(!string.IsNullOrEmpty(str));
    }

    [ContractAbbreviator]
    public static void NotNullOrEmpty(IEnumerable<T> sequence) {
        Contract.Requires<ArgumentNullException>(sequence != null);
        Contract.Requires<ArgumentNullException>(sequence.Any());
    }
}

public static class Ensures {
    [ContractAbbreviator]
    public static void NotNull(){
        Contract.Ensures(Contract.Result<object>() != null);
    }
}

These can be used like this:

public List<SentMessage> EmailAllFriends(Person p) {
    Requires.NotNull(p); //check if object is null
    Requires.NotNullOrEmpty(p.EmailAddress); //check if string property is null or empty
    Requires.NotNullOrEmpty(p.Friends); //check if sequence property is null or empty
    Ensures.NotNull(); //result object will not be null

    //Do stuff
}

ContractArgumentValidatorAttribute I haven't used this one outside of tutorials, but basically it lets you write package several if (test) throw new ArgumentException() calls in a single call that behaves like a call to Contract.Requires. Since it only deals with argument validation, it wouldn't help with your post-condition example.

Answer 5

Contract have conditional compilation flag on them. In release more you code

if condition
    contract
return

becomes

if condition
   return

do you see the problem now?