“Spec# is a formal language for API contracts (influenced by JML, AsmL, and Eiffel), which extends C# with constructs for non-null types, preconditions, postconditions, and object invariants.”
“Code Contracts is a library which provides a language-agnostic way to express coding assumptions in .NET programs and would be included as part of the base class library in .NET 4.0. The contracts can be called as a subset of Spec# and take the form of preconditions, postconditions, and object invariants”
Let’s see how an we leverage code contracts. After installing the code contracts create a new VS Project (I used a console app here) and add the reference to ‘Microsoft.Contracts.dll’, which you would find in ProgramFiles\Microsoft\Contracts\PublicAssemblies\v3.5.
Then enable the Static Contract checking in VS (which is the whole purpose of contracts, validating things at compile time rather than runtime). Goto –> Project Properties and you check the options as shown below :
Now lets see some quick examples of precoditions, postconditions and object invariants . . .
Preconditions - What does it expect?
As the name suggests, precoditions are contracts to ensure that the expected data is provided while performaing an operation.
Postconditions - What does it guarantee?
Postconditions are contracts to ensure certain conditions are met just before exiting an operation.
Object Invariants - What does it maintain?
Object invariants express the conditions under which the object is in a good state.