Part 2
Some Examples
Bear in mind, there are additional overloads for most/all of the following procedures.
Be sure to check them out.
Examples of Preconditions
Contract.Assert
Ensures that a condition is true when in debug mode.
Contract.Assert(MyInput != null);
Contract.Assume
Instructs code analysis tools to assume that the condition supplied as an argument is true, even if it can not be statically proven to always be true.
Good example of how this can be used.
Contract.Assume(MyInput != null);
Contract.Requires
Must be at the beginning of a method or property. Ensures that a condition is true before any other code.
The following example ensures that MyInput parameter is valid (not null in this case) before any other code is run on the same thread.
Contract.Requires(MyInput != null);
Contract.EndContractBlock
Is used to inform the compiler to treat all code before it as if it was a code contract.
This is useful for legacy code.
For example if you have parameter validation code that does not use Code Contract’s.
The contract tools recognise if/then/throw statements as preconditions when the statements appear first inside a method or property,
and the set of such statements are followed by a Contract method call, such as Requires, Ensures, EnsuresOnThrow or EndContractBlock.
if(MyInput == null) throw new NullReferenceException("The input is null"); Contract.EndContractBlock();
Examples of Postconditions
Contract.Ensures
Ensures that a condition is true on exit of a method or property.
Contract.Ensures(0 <= speed && speed <= 800);
Contract.EnsuresOnThrow
This method call must be at the beginning of a method or property, before any other code.
If an exception is thrown, the specified condition must be true and the exception being thrown is of the specified type parameter.
public bool AddAndProcessItem(T item) { Contract.EnsuresOnThrow(!item.Added); try { // add item to a collection and set it's Added property to true } catch (AdditionException) { item.Added = false; throw; } // ... other operations return true; }
Contract.ForAll
Allows the iteration through a collection to ensure all members meet a specific requirement.
// first param MyCollection is of type IEnumerable // second param is a delegate, or lambda (often called a predicate when used like this) Contract.ForAll(MyCollection, x=>x!=null);
Object Invariants
Used to mark methods that contain object invariant specifications.
Defined by decorating a method with the ContractInvariantMethodAttribute.
ContractInvariantMethodAttribute can only be used on a single method per class.
The method must return void and carry out no operations other than a sequence of calls to Contract.Invariant
[ContractInvariantMethod] void ObjectInvariant () { Contract. Invariant ( _y >= 0 ); Contract. Invariant ( _x > _y ); ... }
Code Contract Values
There are also some useful pseudo variables that can be used when writing postconditions.
Contract.Result
A methods or properties return value can be refered to by Contract.Result<T>()
Contract.Result<T>() can be used only in the conditional expression for the Ensures contract.
Methods with a return type of void cannot refer to Contract. Result<T>() within their postconditions for the obvious reason.
Contract.Ensures(0 < Contract.Result());
Contract.OldValue
Contract.OldValue<T>(T value) can be used only in the conditional expression for the Ensures contract.
The generic type argument may be omitted whenever the compiler is able to infer its type.
There are a few restrictions around the use of OldValue. Have a look at the User Manual document. Listed at the end of the post.
Contract.Ensures(MyInput != Contract.OldValue(MyInput));
Pure
Using the PureAttribute indicates that a type, method, property, etc is pure, that is, It has no visible side-effects for callers.
You can only use a method/property/etc in a contract if it is declared Pure.
If the method/property/etc is not decorated with this attribute when called from within a contract, a warning will be given “Detected call to impure method”.
See this post, it has a good example.
Interface Contracts
Contracts for interfaces must be defined in a separate class decorated with the ContractClassForAttribute.
The interface sporting the contract must be decorated with the ContractClassAttribute specifying the type that has the interfaces contract.
The class that implements the interfaces contract is expected to be abstract.
The User Manual listed at the end of this post has some good examples of how to set up Interface Contracts.
[ContractClass(typeof(ContractForInteface))] interface IDoSomething { int DoSomething(int value); } [ContractClassFor(typeof(IDoSomething))] sealed class ContractForInteface : IDoSomething { int IDoSomething.DoSomething(int value) { Contract.Requires( value != 0); //contracts require a dummy value return default(int); } }
There’s plenty of good documentation around Code Contracts
System.Diagnostics.Contracts Namespace
http://msdn.microsoft.com/en-us/library/system.diagnostics.contracts.aspx
The Contract Class
http://msdn.microsoft.com/en-us/library/system.diagnostics.contracts.contract.aspx
Brief description of Code Contracts and how to use them
http://msdn.microsoft.com/en-us/library/dd264808.aspx
The User Manual
http://download.microsoft.com/download/C/2/7/C2715F76-F56C-4D37-9231-EF8076B7EC13/userdoc.pdf
Code Contracts on DevLabs
http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx
DimeCasts has a few web casts on Code Contracts
http://dimecasts.net/Casts/ByTag/Code%20Contracts
Tags: Architecture, Microsoft
November 4, 2010 at 10:13 |
The older I grow the more I distrust the familiar doctrine that age brings wisdom.
April 13, 2012 at 11:42 |
[…] LSP / DbC and .NET’s support part 2 […]
December 1, 2012 at 23:06 |
[…] LSP / DbC and .NET’s support part 2 […]