CODEWITHSUNDEEP
c#code-contracts
Tigran
Tigran

Reputation: 62256

Preconditions and Postconditions in CodeContracts

If I write 

 [Pure]
 static string s10 {get;set;}

 static void Main(string[] args)
 {
     Contract.Ensures(s10.Length <= 10); //Contract fails
     s10 = ";uhlakushdflausgdflasgdfljgaskdjgfasd";
 }

As I don't have Premium edition of VS, so no static checking, after run program VS reports me problem: Postcondition failed: s10.Length <= 10, good.

if I write, instead 

 [Pure]
 static string s10 {get;set;}

 static void Main(string[] args)
 {
    Contract.Requires(s10.Length <= 10); //NullReferenceException
    s10 = ";uhlakushdflausgdflasgdfljgaskdjgfasd";
 }

VS reports me Null reference exception.

Does it actually mean, that as Ensures is postcondition dirrective, even if I put its call like a first line of my method, it will be validated like last one, just before exiting the function ?

Upvotes: 1

Views: 1153

Answers (1)

Jon Skeet
Jon Skeet

Reputation: 1500675

Yes - the Code Contracts rewriter moves the code around to the appropriate place, as well as a few other things. It's worth looking at the result in Reflector to see what's going on.

I strongly advise you to read the user guide that comes with Code Contracts thoroughly. From what I remember, it's an excellent bit of documentation.

Upvotes: 3

Related Questions