c# - 如何在 .NET Core 中正确使用代码契约

Question

我想知道如何在.NET Core中正确使用Code Contracts，目前我尝试将CC添加到我的项目中，编译和调试。我对消息感到困惑，它出现在每个使用 Contract.Requires 的调用中，以及通过谷歌搜索找到的信息。

消息指出:

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 ....

正如我所看到的，项目属性中没有 CC 选项，而且正如我所看到的，CC 的 Github 存储库快死了。有什么方法可以在 .NET Core 中成功使用 CC？

如果没有，有什么简单的方法可以替换它们吗？我用 Contract.Requires和 ContractClassAttribute .替换 Contract.Requires很明显，但是 ContractClassAttribute 让我大吃一惊:-)

Answer 1

首先，根据microsoft docs，让我们了解什么是CodeContracts :

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.

意思是，为了让事情变得简单，CodeContracts 帮助我们简化代码中的测试。

我们如何使用代码契约？

考虑这个例子:

if ( x == null ) throw new ...  
Contract.EndContractBlock(); // All previous "if" checks are preconditions  

两种情况之一的先决条件是什么意思？

• 语句出现在方法中任何其他语句之前。
• 整套这样的陈述后跟一个明确的Contract。方法调用，例如调用 Requires , Ensures , EnsuresOnThrow , 或 EndContractBlock方法。

当 if-then-throw语句以这种形式出现，工具将它们识别为遗留要求语句。如果没有其他合约遵循 if-then-throw 序列，则以 Contract.EndContractBlock 结束代码方法。

---

您也可以在后置条件中使用它:

什么是后置条件？

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.

意思是，简而言之，后置条件帮助我们测试我们的方法。

一个例子是:

Contract.Ensures( this.F > 0 );

请注意特殊的后置条件:

• 您可以使用表达式 Contract.Result<T>() 在后置条件中引用方法返回值, 其中T被方法的返回类型取代。当编译器无法推断类型时，您必须明确提供它。
• 后置条件中的前置值指的是方法或属性开始处的表达式值。它使用表达式 Contract.OldValue<T>(e) , 其中T是 e 的类型.只要编译器能够推断其类型，您就可以省略泛型类型参数。 (例如，C# 编译器总是推断类型，因为它接受一个参数。)对于 e 中可以出现的内容以及旧表达式可能出现的上下文有一些限制。旧表达式不能包含另一个旧表达式。最重要的是，旧表达式必须引用方法的前提条件状态中存在的值。换句话说，它必须是一个表达式，只要方法的前提条件为真，它就可以被计算。

---

最后你有了不变量:

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.

意思是，不变量有助于测试我们的类代码和实例。

一个例子是:

[ContractInvariantMethod]  
protected void ObjectInvariant ()   
{  
Contract.Invariant(this.y >= 0);  
Contract.Invariant(this.x > this.y);  
...  
}  

---

正确使用 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;
    }
}