First of all, let's understand what CodeContracts are, according to microsoft docs:
Code contracts provide a way to specify preconditions, postconditions,
and object invariants in your code. Preconditions are requirements
that must be met when entering a method or property. Postconditions
describe expectations at the time the method or property code exits.
Object invariants describe the expected state for a class that is in a
good state.
Meaning, to make things simple, CodeContracts help us simplify tests in our code.
How do we use code contracts?
Consider this example:
if ( x == null ) throw new ...
Contract.EndContractBlock(); // All previous "if" checks are preconditions
What does it mean by preconditions one of two cases?
When if-then-throw statements appear in this form, the tools recognize them as legacy requires statements. If no other contracts follow the if-then-throw sequence, end the code with the Contract.EndContractBlock method.
You can use it also in Postconditions:
What are Postconditions?
Postconditions are contracts for the state of a method when it
terminates. The postcondition is checked just before exiting a method.
The run-time behavior of failed postconditions is determined by the
runtime analyzer.
Unlike preconditions, postconditions may reference members with less
visibility. A client may not be able to understand or make use of some
of the information expressed by a postcondition using private state,
but this does not affect the client's ability to use the method
correctly.
Meaning, to make things short, Postconditions help us test our methods.
an Example would be:
Contract.Ensures( this.F > 0 );
Please note special postcontions:
- You can refer to method return values in postconditions by using the expression
Contract.Result<T>(), where T is replaced by the return type of the method. When the compiler is unable to infer the type, you must explicitly provide it.
- A prestate value in a postcondition refers to the value of an expression at the start of a method or property. It uses the expression
Contract.OldValue<T>(e), where T is the type of e. You can omit the generic type argument whenever the compiler is able to infer its type. (For example, the C# compiler always infers the type because it takes an argument.) There are several restrictions on what can occur in e and the contexts in which an old expression may appear. An old expression cannot contain another old expression. Most importantly, an old expression must refer to a value that existed in the method's precondition state. In other words, it must be an expression that can be evaluated as long as the method's precondition is true.
Finally you have Invariants:
Object invariants are conditions that should be true for each instance
of a class whenever that object is visible to a client. They express
the conditions under which the object is considered to be correct.
Meaning, Invariants help test our class code and instances.
An example would be:
[ContractInvariantMethod]
protected void ObjectInvariant ()
{
Contract.Invariant(this.y >= 0);
Contract.Invariant(this.x > this.y);
...
}
Full example for proper use of CodeContracts:
using System.Collections.Generic;
using System.Text;
using System.Threading.Tasks;
using System.IO;
using System.Net.Http.Headers;
using System.Diagnostics.Contracts;
namespace System.Net.Http
{
public class FormUrlEncodedContent : ByteArrayContent
{
public FormUrlEncodedContent(IEnumerable<KeyValuePair<string, string>> nameValueCollection)
: base(GetContentByteArray(nameValueCollection))
{
Headers.ContentType = new MediaTypeHeaderValue("application/x-www-form-urlencoded");
}
private static byte[] GetContentByteArray(IEnumerable<KeyValuePair<string, string>> nameValueCollection)
{
if (nameValueCollection == null)
{
throw new ArgumentNullException(nameof(nameValueCollection));
}
Contract.EndContractBlock();
// Encode and concatenate data
StringBuilder builder = new StringBuilder();
foreach (KeyValuePair<string, string> pair in nameValueCollection)
{
if (builder.Length > 0)
{
builder.Append('&');
}
builder.Append(Encode(pair.Key));
builder.Append('=');
builder.Append(Encode(pair.Value));
}
return HttpRuleParser.DefaultHttpEncoding.GetBytes(builder.ToString());
}
private static string Encode(string data)
{
if (String.IsNullOrEmpty(data))
{
return String.Empty;
}
// Escape spaces as '+'.
return Uri.EscapeDataString(data).Replace("%20", "+");
}
internal override Stream TryCreateContentReadStream() =>
GetType() == typeof(FormUrlEncodedContent) ? CreateMemoryStreamForByteArray() : // type check ensures we use possible derived type's CreateContentReadStreamAsync override
null;
}
}
