如何在.NET Core中正确使用代码协定

本文介绍了如何在.NET Core中正确使用代码协定的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！ 问题描述

我想知道如何在 .NET Core 中正确使用代码协定，到目前为止，我试图将CC添加到我的项目中，进行编译和调试。我对消息感到困惑，该消息出现在每个使用 Contract.Requires 的呼叫中，以及通过谷歌搜索找到的信息。

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.

消息指出：

必须使用代码协定重写程序集二进制重写器（CCRewrite），因为它正在调用 Contract.Requires< TException> 和 CONTRACTS_FULL 符号。从项目中删除 CONTRACTS_FULL 符号的所有显式定义，然后重新生成。 CCRewrite ....

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存储库是快死了

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?

如果没有，有什么简单的方法可以替换它们？我使用 Contract.Requires 和 ContractClassAttribute 。替换 Contract.Requires 很明显，但是 ContractClassAttribute 让我很震惊：-）

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 :-)

推荐答案

首先，根据微软文档：

代码合同提供一种在代码中指定前置条件，后置条件，和对象不变式的方法。前提条件是输入方法或属性时必须满足的要求。后置条件描述了方法或属性代码退出时的期望。 对象不变量描述处于良好状态的类的预期状态。

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帮助我们简化了代码中的测试。

Meaning, to make things simple, CodeContracts help us simplify tests in our code.

我们如何使用代码合约？

请考虑以下示例：

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

前提条件是什么两种情况之一？

• 该语句在方法中的任何其他语句之前出现。
• 在此类语句的整个集合之后紧跟一个明确的合同方法调用，例如对要求，确保， EnsuresOnThrow 或 EndContractBlock 方法。

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

当 if-then-throw 语句以这种形式出现时，工具会将其识别为旧版require语句。如果没有其他合同遵循if-then-throw序列，则以 Contract.EndContractBlock 方法。

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.

您还可以在后置条件中使用它：

什么是后置条件？

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.

与先决条件不同，后置条件可以引用$ b $较少的成员b能见度。客户可能无法理解或利用后置条件使用私有状态表示的某些信息，但这不会影响客户正确使用方法的能力。

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.

例如：

Contract.Ensures( this.F > 0 );

请注意特殊的后置条件：

Please note special postcontions:

• 您可以使用表达式 Contract.Result< T>（）来引用后置条件中的方法返回值，其中 T 替换为方法的返回类型。当编译器无法推断类型时，必须显式提供它。
• 后置条件中的前状态值是指方法或属性开始处的表达式的值。它使用表达式 Contract.OldValue< T>（e），其中 T 是 e 。只要编译器能够推断其类型，就可以省略泛型类型参数。 （例如，C＃编译器始终会推断类型，因为它需要一个参数。）对于e中可能发生的情况以及可能会出现旧表达式的上下文有一些限制。一个旧表达式不能包含另一个旧表达式。最重要的是，旧表达式必须引用方法的前提条件状态中存在的值。换句话说，只要该方法的前提为true，它就必须是可以计算的表达式。

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

最后，您具有不变式：

对象不变式是条件，对于每个实例只要该对象对客户端可见，则为class。他们表达认为对象正确的条件。

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.

例如：

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