How to properly use Code Contracts in .NET Core

Question

I wonder, how to properly use Code Contracts in .NET Core, so far I tried to add CC to my project, compile and debug. I'm confused by message, which is appearing in each call which uses Contract.Requires, and information found by googling.

The message states:

An assembly must be rewritten using the code contracts binary rewriter (CCRewrite) because it is calling Contract.Requires<TException> and CONTRACTS_FULL symbol is defined. Remove any explicit definitions of the CONTRACTS_FULL symbol from your project and rebuild. CCRewrite ....

As I can see there are no CC options in the project properties and as I can see CC's Github repository is nearly dead. Is the are any way how to successfully use CC in .NET Core?

And if not, is there any simple way how to replace them? I use Contract.Requires and ContractClassAttribute. Replacing Contract.Requires is obvious, but ContractClassAttribute is blowing my mind :-)

Answer 1

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?

• The statements appear before any other statements in a method.
• The entire set of such statements is followed by an explicit Contract method call, such as a call to the Requires, Ensures, EnsuresOnThrow, or EndContractBlock method.

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;
    }
}

Answer 2

The answer is: Code Contracts is no longer supported for .NET Core. It's available in the .NET Core 2.0, but it's no longer maintained.

See the official statement at the docs page:

Note

Code contracts aren't supported in .NET 5+ (including .NET Core versions). Consider using Nullable reference types instead.

Also on Github thread (Are Code Contracts going to be supported in .NET Core going forwards? #6361):

We have stopped investing in code contracts a while ago. We've added it to .NET Core 2.0 as part of our compatibility effort, but I wouldn't recommend new code using it.

FWIW, we've looked at many code bases that use them and it seems the overwhelming usage is about null handling. The replacement for this is under way with C# 8's nullable-reference types.

— Immo Landwerth, Program manager on the .NET team at Microsoft. https://twitter.com/terrajobst