Code Contracts Clause Samples

Code Contracts. With code contracts [1] additional expressivity is brought to .NET interfaces and classes by means of preconditions, postconditions, and object invariants. A method can be equipped with preconditions and postconditions. A precon- dition is a contract on the state of the system when a method is invoked and typically imposes constraints on parameter values. Only if the precondition is satisfied, the method is really executed; otherwise an exception is thrown. In contrast, a postcondition is evaluated when the method terminates, prior to exiting the method. Code contracts provide a Contract class in the name- space System.Diagnostics. Static methods of Contract are used to express preconditions and postconditions. To give an example, consider a method squareRoot that should not accept negative numbers. This could be encoded as follows: using System.Diagnostics.Contract; class MyService { double squareRoot(double d) { Contract.Requires(d >= 0); return Math.Sqrt(d); } } is visible to a client. During runtime checking, invariants are checked at the end of each public method. In order to specify an invariant for a class, an extra method is introduced that is annotated with the attribute ContractInvariantMethod. Within this method, the conditions are defined with the method Contract.Invariant. The above sample shows how preconditions can be ex- pressed for classes. As a method in an interface is described only by its signature and cannot have a body, code contracts foresee a simple trick to encode constraints for interface methods. The required constraints are specified in another class, which is associated with the interface. Suppose a class AContract should implement code contracts for an interface IA. Then IA is annotated with the attribute [ContractClass(typeof(AContract))], and AContract is equipped with [ContractClass- For(typeof(IA))]. Now the code contracts of ACon- tract apply to the interface IA. Note that most methods of the Contract class are conditionally compiled. It can be configured via symbols to which degree code contracts should be applied during compilation. Code contracts can be completely turned on (full checking) and off (all Contract methods are ignored); it is also possible to check only selected code contracts constraints such as preconditions.