“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.
e.g. :
Postconditions - What does it guarantee? Postconditions are contracts to ensure certain conditions are met just before exiting an operation.
e.g. :
Object Invariants - What does it maintain? Object invariants express the conditions under which the object is in a good state.
e.g. :
(In the above customer class we have an invariant contract to check that the ID should always be greater than zero, which is being called after each public method calls and validated)
Interface Contracts
Code contracts can also be applied to Interface methods by creating a sealed classes as shown below :
There are many other methods in the Contract class which could be used in many other scenarios. Checkout the documentation of this library and Matthew’s blog post for more details.
No comments:
Post a Comment