views:

582

answers:

1

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);
}
+2  A: 

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

Igor Zevaka
hum, result can be null actually.
Victor Rodrigues
Right, so perhaps `(result == null || result >= 0)`?
Igor Zevaka
More generally, implication `if x then y` is `!x || y`, so here we have `!(result != null) || result >= 0` which simplifies to `result == null || result >= 0`.
Porges