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.
