Code contracts: the missing methods
In the last posts, I’ve been talking extensively about Code Contracts. If you’re a reader of this blog, you know that I’m hooked on it. I’ve just been reviewing the previous posts and I’ve noticed that I didn’t mention the Assert and Assume methods. Both are used for testing state and assumptions on a specific point of the program. As you might expect, they follow the same syntax as the other methods that have been presented in the past.
Interestingly, both methods let you use members with less visibility than the method where you’re using them. At runtime, both have the same behavior and will only delegate to the Assert method of the runtime rewriter when you define the CONTRACTS_FULL constant on your code. btw, by default the predefined rewriter will call the Debug.Assert method.
The Assume method is interesting, especially when you think about the static analysis step. All the assumptions that you add (ie, every Assume method call) will be added to the “known facts” list maintained by the static validation tool and will be used by it to check other existing contracts on that scope. What this means is that you should use Assume for giving the validation tool more info about some facts which you know to be true at runtime, but that won’t be inferred by the static analysis tool.
The best way to test this concepts is to run a small example and start adding Assert and Assume method calls. Unfortunately, I didn’t had the necessary time for building such a sample,so you’ll have to do it yourself….