碼上快樂

相關內容    簡體    繁體

c#Code Contracts代碼協定

本文轉載自   查看原文   2017-07-11 16:10   2224    C#

Code Contracts的命名空間：System.Diagnostics.Contracts

集合1.

安裝Code Contracts for .NET插件
Contracts.devlab9ts.msi

安裝了該插件后，可以在項目的屬性頁上發現多了一個Code Contracts的標簽：

勾上"Perform Runtime Check"選項,只是可以看到右側的下拉框有五個選項，這里分別介紹一下它們的區別：

  1. Full表示執行所有的代碼協定語句。
  2. Pre and Post表示執行前置和后置條件檢查，即Contract.Require和Contract.Ensures。
  3. Preconditions 表示只執行前置條件檢查，即Contract.Require。
  4. ReleaseRequires 表示執行public類的public方法的前置條件檢查。
  5. None表示不執行代碼協定檢查，即不進行代碼協定注入。

之所以有這些選項，是因為代碼協定的代碼注入運行時候是有開銷的，影響運行性能。另外，鏈接的時候注入代碼也是影響程序的生成時間的。我們可以在需要檢驗功能的時候放開代碼檢查，需要性能的時候關閉檢查，非常方便，而傳統的手動拋異常的方式就做不到這一點。

值得一提的是，它是可以在Debug版本和Release版本中選擇不同的開關的。我們在Debug版本中開啟必要的代碼檢查，而在Release版本中關閉檢查。需要注意的是，public類的public方法的入參檢查（前置條件協定）是有必要的，即使在Release版本中也也應該存在。我的個人建議是在Debug版本中平時使用Pre and Post選項（注入代碼也是影響程序的生成時間的，故只在有必要的時候才使用Full的方式），在Release版本中使用ReleaseRequires選項。

另外，在安裝了Code Contracts for .NET插件后，它也順帶安裝了一些代碼片段，方便我們快速輸入，非常給力。例如Contract.Require函數可以直接通過"cr"+Tab鍵輸入，Contract.Ensures可以通過"ce"+Tab鍵輸入。

 

集合2.

Project Setup

After you’ve downloaded and installed Code Contracts and created a library project, you need to enable CC for that library. Under the Project Properties, there is a new tab called Code Contracts. Here’s the way that I like to set it up:

  • Set “Assembly Mode” to “Standard Contract Requires”.
  • Debug - Check “Perform Runtime Contract Checking” and set to “Full”. Check “Call-site Requires Checking”.

  • Release - Set “Contract Reference Assembly” to “Build” and check “Emit contracts into XML doc file”.

In addition, if you have the Academic or Commercial Premium edition of Code Contracts, add a configuration called CodeAnalysis with all the settings from Debug and also check “Perform Static Contract Checking” and all the other checkboxes in that section except “Baseline”.

This will give you three separate builds, with separate behavior:

  • CodeAnalysis - This evaluates all the code contracts at build time, searching for any errors. This “build” doesn’t result in a usable dll, but should be run before checking in code, similar to a unit test.
  • Debug - This turns on all code contracts at runtime. This includes code contract checks for any libraries that your library uses (such as CLR libraries). It also turns on consistency checks such as Contract.Assert and ContractInvariantMethod.
  • Release - This turns off all code contracts in your dll at runtime. However, it includes a separate “.Contracts.dll” which contains the contracts for your library’s public API.

Projects consuming your library should reference your Release build. In their Debug configuration, they should check “Perform Runtime Contract Checking” and “Call-site Requires Checking”; this will ensure that the code contracts for your library’s public API are enforced at runtime (the “Call-site” option uses the “.Contracts.dll” assembly that you built). In their Release configuration, they should leave code contracts disabled, which allows all assemblies to run at full speed.

If the consuming project suspects a bug in your library (i.e., their Debug build doesn’t cause any Contracts violations but your library is still not behaving as expected), they can remove the reference to your Release build and add a reference to your Debug build. This is an easy way to enable all the code contract checks in your library, even the internal ones.

Preconditions (Contract.Requires)

Preconditions require some condition at the beginning of a method. Common examples are requiring a parameter to be non-null, or to require the object to be in a particular state.

public string GetObjectInfo(object obj) { Contract.Requires(obj != null); return obj.ToString(); }

Postconditions (Contract.Ensures)

Postconditions guarantee some condition at the end of a method. It is often used with Contract.Result to guarantee that a particular method won’t return null.

private string name; // never null public string Name { get { Contract.Ensures(Contract.Result<string>() != null); return this.name; } }

Preconditions and Postconditions on Interfaces

Both preconditions and postconditions are commonly placed on interface members. Code Contracts includes the ContractClassAttribute and ContractClassForAttribute to facilitate this:

[ContractClass(typeof(MyInterfaceContracts))] public interface IMyInterface { string GetObjectInfo(object obj); string Name { get; } } [ContractClassFor(typeof(IMyInterface))] internal abstract class MyInterfaceContracts : IMyInterface { public string GetObjectInfo(object obj) { Contract.Requires(obj != null); return null; // fake implementation } public string Name { get { Contract.Ensures(Contract.Result<string>() != null); return null; // fake implementation does not need to satisfy postcondition } } }

With generic interfaces, the same idea holds:

[ContractClass(typeof(MyInterfaceContracts<,>))] public interface IMyInterface<T, U> { string GetObjectInfo(object obj); string Name { get; } } [ContractClassFor(typeof(IMyInterface<,>))] internal abstract class MyInterfaceContracts<T, U> : IMyInterface<T, U> { public string GetObjectInfo(object obj) { Contract.Requires(obj != null); return null; // fake implementation } public string Name { get { Contract.Ensures(Contract.Result<string>() != null); return null; // fake implementation does not need to satisfy postcondition } } }

Invariants (ContractInvariantMethod, Contract.Invariant)

Object invariants are expressed using the ContractInvariantMethod. If they are enabled by the build, then they are checked at the beginning of each method (except constructors) and at the end of each method (except Dispose and the finalizer).

public class MyClass<T, U>: public IMyInterface<T, U> { private string name; public MyClass(string name) { Contract.Requires(name != null); this.name = name; }  [ContractInvariantMethod] private void ObjectInvariant() { Contract.Invariant(this.name != null); } public string Name { get { Contract.Ensures(Contract.Result<string>() != null); return this.name; } } public string GetObjectInfo(object obj) { Contract.Requires(obj != null); return obj.ToString(); } }

Assertions and Assumptions (Contract.Assert, Contract.Assume)

There will always be some things that should be true but just have to be checked at runtime. For these, use Contract.Assert unless the static checker (i.e., the CodeAnalysis configuration) complains. You can then change them to be Contract.Assume so that the static checker can use them. There’s no difference between Contract.Assert and Contract.Assume at runtime.

Reminder: if you’re using the Release build setup recommended above, then all your Contract.Assertand Contract.Assume calls get removed from your release builds. So they can’t be used to throw vexing exceptions, e.g., rejecting invalid input.

In the example below, the static checker would complain because Type.MakeGenericType has preconditions that are difficult to prove. So we give it a little help by inserting some Contract.Assumecalls, and the static checker is then pacified.

public static IMyInterface<T, U> CreateUsingReflection() { var openGenericReturnType = typeof(MyClass<,>); Contract.Assume(openGenericReturnType.IsGenericTypeDefinition); Contract.Assume(openGenericReturnType.GetGenericArguments().Length == 2); var constructedGenericReturnType = openGenericReturnType.MakeGenericType(typeof(T), typeof(U)); return (IMyInterface<T, U>)Activator.CreateInstance(constructedGenericReturnType); }

For More Information

The Code Contracts library has a thorough user manual available. It’s a bit of a hard read, but they include a lot of information that I’ve skipped for this “intro” post, such as:

  • Specifying postconditions that hold even if the method throws an exception.
  • Techniques for gradually migrating Code Contracts into an existing library.
  • Details on how Code Contracts are inherited.
  • Contract abbreviations.
  • Applying contracts to sequences (e.g., ForAll and Exists quantifiers).
  • Advanced contract checking with Pure methods.
  • Tips for working with the static checker.

集合3

1. Assert

Assert(斷言)是最基本的契約。.NET 4.0 使用 Contract.Assert() 方法來特指斷言。它用來表示程序點必須保持的一個契約。

Contract.Assert(this.privateField > 0);
Contract.Assert(this.x == 3, "Why isn’t the value of x 3?");

 

斷言有兩個重載方法，首參數都是一個布爾表達式，第二個方法的第二個參數表示違反契約時的異常信息。

當斷言運行時失敗，.NET CLR 僅僅調用 Debug.Assert 方法。成功時則什么也不做。

2. Assume

.NET 4.0 使用 Contract.Assume() 方法表示 Assume(假設) 契約。

Contract.Assume(this.privateField > 0);
Contract.Assume(this.x == 3, "Static checker assumed this");

Assume 契約在運行時檢測的行為與 Assert(斷言) 契約完全一致。但對於靜態驗證來說，Assume 契約僅僅驗證已添加的事實。由於諸多限制，靜態驗證並不能保證該契約。或許最好先使用 Assert 契約，然后在驗證代碼時按需修改。

當 Assume 契約運行時失敗時， .NET CLR 會調用 Debug.Assert(false)。同樣，成功時什么也不做。

3. Preconditions

.NET 4.0 使用 Contract.Requires() 方法表示 Preconditions(前置條件) 契約。它表示方法被調用時方法狀態的契約，通常被用來做參數驗證。所有 Preconditions 契約相關成員，至少方法本身可以訪問。

Contract.Requires(x != null);

Preconditions 契約的運行時行為依賴於幾個因素。如果只隱式定義了 CONTRACTS PRECONDITIONS 標記，而沒有定義 CONTRACTS_FULL 標記，那么只會進行檢測 Preconditions 契約，而不會檢測任何 Postconditions 和 Invariants 契約。假如違反了 Preconditions 契約，那么 CLR 會調用 Debug.Assert(false) 和 Environment.FastFail 方法。

假如想保證 Preconditions 契約在任何編譯中都發揮作用，可以使用下面這個方法：

Contract.RequiresAlways(x != null);

為了保持向后兼容性，當已存在的代碼不允許被修改時，我們需要拋出指定的精確異常。但是在 Preconditions 契約中，有一些格式上的限定。如下代碼所示：

if (x == null) throw new ArgumentException("The argument can not be null.");
Contract.EndContractBlock();    // 前面所有的 if 檢測語句皆是 Preconditions 契約

 

這種 Preconditions 契約的格式嚴格受限：它必須嚴格按照上述代碼示例格式。而且不能有 else 從句。此外，then 從句也只能有單個 throw 語句。最后必須使用 Contract.EndContractBlock() 方法來標記 Preconditions 契約結束。

看到這里，是不是覺得大多數參數驗證都可以被 Preconditions 契約替代？沒有錯，事實的確如此。這樣這些防御性代碼完全可以在 Release 被去掉，從而不用做那些冗余的代碼檢測，從而提高程序性能。但在面向驗證客戶輸入此類情境下，防御性代碼仍有必要。再就是，Microsoft 為了保持兼容性，並沒有用 Preconditions 契約代替異常。

4. Postconditions

Postconditions 契約表示方法終止時的狀態。它跟 Preconditions 契約的運行時行為完全一致。但與 Preconditions 契約不同，Postconditions 契約相關的成員有着更少的可見性。客戶程序或許不會理解或使用 Postconditions 契約表示的信息，但這並不影響客戶程序正確使用 API 。

對於 Preconditions 契約來說，它則對客戶程序有副作用：不能保證客戶程序不違反 Preconditions 契約。

A. 標准 Postconditions 契約用法

.NET 4.0 使用 Contract.Ensures() 方法表示標准 Postconditions 契約用法。它表示方法正常終止時必須保持的契約。

Contract.Ensures(this.F > 0);
B. 特殊 Postconditions 契約用法

當從方法體內拋出一個特定異常時，通常情況下 .NET CLR 會從方法體內拋出異常的位置直接跳出，從而輾轉堆棧進行異常處理。假如我們需要在異常拋出時還要進行 Postconditions 契約驗證，我們可以如下使用：

Contract.EnsuresOnThrows<T>(this.F > 0);

其中小括號內的參數表示當異常從方法內拋出時必須保持的契約，而泛型參數表示異常發生時拋出的異常類型。舉例來說，當我們把 T 用 Exception 表示時，無論什么類型的異常被拋出，都能保證 Postconditions 契約。哪怕這個異常是堆棧溢出或任何不能控制的異常。強烈推薦當異常是被調用 API 一部分時，使用 Contract.EnsuresOnThrows<T>() 方法。

C. Postconditions 契約內的特殊方法

以下要講的這幾個特殊方法僅限使用在 Postconditions 契約內。

方法返回值 在 Postconditions 契約內，可以通過 Contract.Result<T>() 方法表示，其中 T 表示方法返回類型。當編譯器不能推導出 T 類型時，我們必須顯式指出。比如，C# 編譯器就不能推導出方法參數類型。

Contract.Ensures(0 < Contract.Result<int>());

 

假如方法返回 void ，則不必在 Postconditions 契約內使用 Contract.Result<T>() 。

前值(舊值)  在 Postconditions 契約內，通過 Contract.OldValue<T>(e) 表示舊有值，其中 T 是 e 的類型。當編譯器能夠推導 T 類型時，可以忽略。此外 e 和舊有表達式出現上下文有一些限制。舊有表達式只能出現在 Postconditions 契約內。舊有表達式不能包含另一個舊有表達式。一個很重要的原則就是舊有表達式只能引用方法已經存在的那些舊值。比如，只要方法 Preconditions 契約持有，它必定能被計算。下面是這個原則的一些示例：

  • 方法的舊有狀態必定存在其值。比如 Preconditions 契約暗含 xs != null ，xs 當然可以被計算。但是，假如 Preconditions 契約為 xs != null || E(E 為任意表達式)，那么 xs 就有可能不能被計算。
Contract.OldValue(xs.Length);  // 很可能錯誤
  • 方法返回值不能被舊有表達式引用。
Contract.OldValue(Contract.Result<int>() + x);  // 錯誤
  • out 參數也不能被舊有表達式引用。
  • 如果某些標記的方法依賴方法返回值，那么這些方法也不能被舊有表達式引用。
Contract.ForAll(0, Contract.Result<int>(), i => Contract.OldValue(xs[i]) > 3);  // 錯誤
  • 舊有表達式不能在 Contract.ForAll() 和 Contract.Exists() 方法內引用匿名委托參數，除非舊有表達式被用作索引器或方法調用參數。
Contract.ForAll(0, xs.Length, i => Contract.OldValue(xs[i]) > 3);  // OK

 

Contract.ForAll(0, xs.Length, i => Contract.OldValue(i) > 3);  // 錯誤
  • 如果舊有表達式依賴於匿名委托的參數，那么舊有表達式不能在匿名委托的方法體內。除非匿名委托是 Contract.ForAll() 和 Contract.Exists() 方法的參數。
Foo( ... (T t) => Contract.OldValue(... t ...) ... ); // 錯誤

 

D. out 參數

因為契約出現在方法體前面，所以大多數編譯器不允許在 Postconditions 契約內引用 out 參數。為了繞開這個問題，.NET 契約庫提供了 Contract.ValueAtReturn<T>(out T t) 方法。

public void OutParam(out int x)
{
    Contract.Ensures(Contract.ValueAtReturn(out x) == 3);
    x = 3;
}

跟 OldValue 一樣，當編譯器能推導出類型時，泛型參數可以被忽略。該方法只能出現在 Postconditions 契約。方法參數必須是 out 參數，且不允許使用表達式。

需要注意的是，.NET 目前的工具不能檢測確保 out 參數是否正確初始化，而不管它是否在 Postconditions 契約內。因此， x = 3 語句假如被賦予其他值時，編譯器並不能發現錯誤。但是，當編譯 Release 版本時，編譯器將發現該問題。

5. Object Invariants

對象不變量表示無論對象是否對客戶程序可見，類的每一個實例都應該保持的契約。它表示對象處於一個“良好”狀態。

在 .NET 4.0 中，對象的所有不變量都應當放入一個受保護的返回 void 的實例方法中。同時用[ContractInvariantMethod]特性標記該方法。此外，該方法體內在調用一系列 Contract.Invariant() 方法后不能再有其他代碼。通常我們會把該方法命名為 ObjectInvariant 。

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

 

同樣，Object Invariants 契約的運行時行為和 Preconditions 契約、Postconditions 契約行為一致。CLR 運行時會在每個公共方法末端檢測 Object Invariants 契約，但不會檢測對象終結器或任何實現 System.IDisposable 接口的方法。

 Contract 靜態類中的其他特殊方法

.NET 4.0 契約庫中的 Contract 靜態類還提供了幾個特殊的方法。它們分別是：

A. ForAll

Contract.ForAll() 方法有兩個重載。第一個重載有兩個參數：一個集合和一個謂詞。謂詞表示返回布爾值的一元方法，且該謂詞應用於集合中的每一個元素。任何一個元素讓謂詞返回 false ，ForAll 停止迭代並返回 false 。否則， ForAll 返回 true 。下面是一個數組內所有元素都不能為 null 的契約示例：

public T[] Foo<T>(T[] array)
{
    Contract.Requires(Contract.ForAll(array, (T x) => x != null));
}

 

B. Exists

它和 ForAll 方法差不多。

 

 

注：摘自

http://www.cnblogs.com/lucifer1982/archive/2009/03/21/1418642.html

http://blog.stephencleary.com/2011/01/simple-and-easy-code-contracts.html

 


免責聲明！

本站轉載的文章為個人學習借鑒使用，本站對版權不負任何法律責任。如果侵犯了您的隱私權益，請聯系本站郵箱yoyou2525@163.com刪除。



猜您在找 XSD與C#Code以及XML之間的相互關心 利用.NET Code Contracts實現運行時驗證 Objective-C 代碼規范（Code Style） C# ORM—Entity Framework 之Code first（代碼優先）（二） C#基礎—不安全代碼(unsafe code) C# 項目引用WebService，提示報錯“在 ServiceModel 客戶端配置部分中，找不到引用協定...” 代碼重構（Code Refactoring） code ELIFECYCLE (代碼周期) vs code 調試C/C++代碼時，不能有中文路徑 VS Code C/C++代碼格式化--大括號'{'不換行
 
粵ICP備18138465號   © 2018-2025 CODEPRJ.COM