I've started reading up on code contracts in c# but despite all the explanations of preconditions and postconditions they fail to mention what they actually DO.
Are they checks or constraints that, if failed during runtime, throw an exception?
Are they checks for design time that raise warnings or errors if their conditions are not satisfied?
The (now abandoned) code contracts feature in C# actually performed either of those two options depending on how it was configured and which version of Visual Studio you were running.
The main intent of code contracts was to prove that certain program states were not possible in any execution. This proof was to be performed at compile time. The main reason for these proofs is to ensure that the program is correct. Ideally, however, this would also allow the removal of any runtime checks associated with impossible program states which would improve performance.
Sometimes this sort of proof wasn't possible, and the constraints would be implemented as ordinary (runtime) assertions. The system could be configured to make all constraints checked at runtime as well.
Additionally, the system could also be configured to ignore all of the constraints.
The contracts code was created after the compilation stage by a re-writer program that operated on the IL code that was output by the compiler. So the original compiler output would be the same regardless of how the code contracts system was configured.
