CsharpThinking---代碼契約CodeContract（八）

本文轉載自查看原文 2013-06-18 11:05 1987 C# 契約編程契約/ 編程開發 - C#

代碼契約（Code Contract）：它並不是語言本身的新功能，而是一些額外的工具，幫助人們控制代碼邊界。

代碼契約之於C#，就相當於詩詞歌賦之於語言。 --- C# in Depth

一，概述

　　1.1 未引入“代碼契約（特指MS代碼契約）”之前的狀態---“契約”

　　　　• 契約：20世紀80年代，Bertand Meyer在設計Eiffel語言時就將其作為重要的部分。已有大量的計算機科學研究開始探究正式的規范說明和驗證，它允許在編譯時檢查程序的正確性，不過契約的作用還不止於此。

　　　　• 契約編程的核心理念是將API的需求和承諾與實現相分離。

　　　　• 契約約定比文檔約定方式更“同步”一些。

　　　　• 或使用Debug.Assert方式，但其不能在Release構建時不會捕獲非法參數。

　　　　　/************************使用代碼契約方式之前*****************************/
　　　　　/// <summary>
        /// Counts the number of whitespace characters in <paramref name="text"/>
        /// </summary>
        /// <param name="text">String to examine. Must not be null.</param>
        /// <example cref="ArgumentNullException"><paramref name="text"/> is null.</example>
        /// <returns>The number of whitespace characters</returns>
        public static int CountWhiteSpace(string text)
        {
            if (string.IsNullOrEmpty(text))
                throw new ArgumentNullException("text");
            return text.Count(char.IsWhiteSpace);
        }

        /************************使用代碼契約方式之前*****************************/
        /// <summary>
        /// 說明:只能在Debug模式下規范”契約“。
        /// </summary>
        /// <param name="text"></param>
        /// <returns></returns>
        public static int CountStringLength(string text)
        {
            // 命名空間：using System.Diagnostics; 
            Debug.Assert(text != null);
            return text.Length;
        }

　1.2 代碼契約

　　　　• C#代碼契約起源於微軟開發的一門研究語言Spec#（參見http://mng.bz/4147）。

　　　　• 契約工具：包括：ccrewrite（二進制重寫器，基於項目的設置確保契約得以貫徹執行）、ccrefgen（它生成契約引用集，為客戶端提供契約信息）、cccheck（靜態檢查器，確保代碼能在編譯時滿足要求，而不是僅僅

　　　　　　　　　　檢查在執行時實際會發生什么）、ccdocgen（它可以為代碼中指定的契約生成xml文檔）。

　　　　• 契約種類：前置條件、后置條件、固定條件、斷言和假設、舊式契約。

　　　 • 代碼契約工具下載及安裝：下載地址Http://mng.bz/cn2k。（代碼契約工具並不包含在Visual Studio 2010中，但是其核心類型位於mscorlib內。）

　　　　• 命名空間：System.Diagnostics.Contracts.Contract

　　　　• 代碼契約優勢：編譯前執行檢查（如若設置異常類型使用EnsuresOnThrow<Exception>則會在編譯時拋出異常），這樣比較編譯后檢查有明顯的優勢。

　　1.3 契約種類介紹

　　　　• 前置條件（precondition）：是對方法調用者提出的要求，而不是表示普通條件下方法本身的行為。Contract.Requires<T>();

 1         /// <summary>
 2         /// 實現“前置條件”的代碼契約
 3         /// </summary>
 4         /// <param name="text">Input</param>
 5         /// <returns>Output</returns>
 6         public static int CountWhiteSpace(string text)
 7         {
 8             // 命名空間：using System.Diagnostics.Contracts;
 9             Contract.Requires<ArgumentNullException>(text != null, "Paramter:text");// 使用了泛型形式的Requires
10             return text.Count(char.IsWhiteSpace);
11         }

　　　　• 后置條件(postcondition)：表示對方法輸出的約束：返回值、out或ref參數的值，以及任何被改變的狀態。Ensures();

        /// <summary>
        /// 實現“前置條件”的代碼契約
        /// </summary>
        /// <param name="text">Input</param>
        /// <returns>Output</returns>
        public static int CountWhiteSpace(string text)
        {
            // 命名空間：using System.Diagnostics.Contracts;
            Contract.Requires<ArgumentNullException>(!string.IsNullOrEmpty(text), "text"); // 使用了泛型形式的Requires
            Contract.Ensures(Contract.Result<int>() > 0); // 1.方法在return之前，所有的契約都要在真正執行方法之前（Assert和Assume除外，下面會介紹）。
                                                          // 2.實際上Result<int>()僅僅是編譯器知道的”占位符“：在使用的時候工具知道它代表了”我們將得到那個返回值“。
            return text.Count(char.IsWhiteSpace);
        }

        public static bool TryParsePreserveValue(string text, ref int value)
        {
            Contract.Ensures(Contract.Result<bool>() || Contract.OldValue(value) == Contract.ValueAtReturn(out value)); // 此結果表達式是無法證明真偽的。
            return int.TryParse(text, out value); // 所以此處在編譯前就會提示錯誤信息：Code Contract：ensures unproven: XXXXX
        }

　　　　• 固定條件（invariant）：它們是只要對象的狀態可見，就必須自始至終遵循的契約。換句話說，在類的公共方法運行時，固定條件可以改變，但在方法的最后，它們仍要滿足契約。

 1         public sealed class CardGame
 2         {
 3             readonly Stack<Card> deck = new Stack<Card>(Card.CreateFullDeck());
 4             readonly Stack<Card> discardPile = new Stack<Card>();
 5             readonly List<Player> players = new List<Player>();
 6 
 7             public void DealCard(Player p)
 8             {
 9                 players.Add(p);
10             }
11 
12             [ContractInvariantMethod]
13             private void ObjectInvarint()
14             {
15                 Contract.Invariant((deck.Count + discardPile.Count + players.Sum(p => p.CardCount)) == Card.FullDeckSize); // 校驗總和是否一致。
16             }
17         }

　　　　　　　　特性：1. 固定條件方法是無參數、無返回值、私有的。

　　　　　　　　　　　2. 用[ContractInvariantMethod]標簽修飾。

　　　　　　　　　　　3. 執行起來代價低廉，不必擔心性能損失。

　　　　　　　　　　　4. 如果檢查集合內容還可用Contract.ForAll or Contarct.Exists.

            [ContractInvariantMethod]
            private void InvarintCollection()
            {
                Contract.Invariant(Contract.ForAll(players, item => item.Name != "Stephen")); // 校驗集合。
                Contract.Invariant(!Contract.Exists(players, item => item.Name != "Stephen")); // 與上句作用相同。
            }

　　　　• 斷言和假設：可檢測在代碼進行到“一半”時發生的事情。

　　　　　　　　斷言Assert：靜態檢查器會檢測Assert是否正確，而Assume不會。大多數情況下使用。

　　　　　　　　假設Assume：正因為靜態檢查器不會檢查，所以某些情況下需要過濾掉靜態檢查器無法檢驗的東西。

            public static int RollDic(Random rng)
            {
                Contract.Ensures(Contract.Result<int>() >= 2);

                if (rng == null)
                    rng = new Random();
                Contract.Assert(rng != null);

                int firstRoll = rng.Next(1, 7);
                Contract.Assume(firstRoll >= 1);
                Contract.Assume(firstRoll <= 6);

                return firstRoll;
            }

　　　　• 舊式契約：本質上是另一種形式的前置條件。DoNet2.0支持。

            public static int CountSpace(string text)
            {
                if (text == null)
                    throw new ArgumentNullException("text");
                Contract.EndContractBlock(); // 此方法不做任何事情，只是讓二進制編譯器知道，此句以上的部分是契約。

                return text.Count(char.IsWhiteSpace);
            }

　　二，使用ccrewrite和ccrefge重寫二進制

　　　 2.1 契約重寫：重寫剛剛獲取的程序集的某些部分，以替換原始的程序集。

　　　　　　替換的事件序列：

　　　　　　　　　　• 檢查前置條件。

　　　　　　　　　　• 為OldValue方法調用獲取初始的狀態。

　　　　　　　　　　• 執行代碼的功能部分，如Assert

• 檢查后置條件

　　　　　　　　　　• 檢查固定條件

　　　　2.2 契約繼承（重要）

　　　　　　• 特性：1. 覆蓋某方法（或實現某個接口方法，規范契約）會繼承該方法中的契約。

　　　　　　　　　2. 不能再繼承的方法中添加額外的前置條件，但卻可以添加固定條件和后置條件。必須符合Liskov替換原則（里氏代換原則http://zh.wikipedia.org/wiki/Liskov%E4%BB%A3%E6%8F%9B%E5%8E%9F%E5%89%87）。

　　　　　 • 繼承：使其子類也有父類中的前置條件、后置條件等，作為一種條件約束，但也有其限制，而且繼承很容易被濫用，不如實現接口方式穩妥。

        [Pure]
        public static bool Report(string text)
        {
            Console.WriteLine(text);
            return true;
        }

        public class ContractBase
        {
            public virtual void VirtualMethod(string text)
            {
                Contract.Requires(Report("Base precondition"));
                Contract.Ensures(Report("Base postcondition"));
            }
        }

        public class Derived : ContractBase
        {
            public override void VirtualMethod(string text)
            {
                Contract.Ensures(Report("Dervied postcondition"));
            }
        }

        /* *******************************************************
         * 結果：
         * Base precondition
         * Dervied postcondition
         * Base postconditon
         * 
         * 注：盡管Dervied中覆寫的方法沒有調用base.VirtualMethod(),
         * 契約仍然被執行。
         * *******************************************************/

　　　　　　• 為接口指定契約：

 1         /*************************************************************
 2          * 說明：
 3          * 1. ICaseConverter與ICaseConverterContracts互為實現（相互反向
 4          *    引用）。
 5          * 2. ICaseConverter只定義接口方法。
 6          * 3. ICaseConverterContracts抽象類中實現接口的約束，內部要定義成
 7          *    私有。
 8          * 4. CurrentCultrueUpperCaseFormatter實現接口ICaseConverter，而
 9          *    與抽象類隔離。
10          * ***********************************************************/
11         /// <summary>
12         /// 接口類
13         /// </summary>
14         [ContractClass(typeof(ICaseConverterContracts))] // 指定契約類
15         public interface ICaseConverter
16         {
17             string Convert(string text);
18         }
19 
20         /// <summary>
21         /// 契約類
22         /// </summary>
23         [ContractClassFor(typeof(ICaseConverter))] // 聲明契約所服務的類型
24         internal abstract class ICaseConverterContracts : ICaseConverter
25         {
26             public string Convert(string text)
27             {
28                 Contract.Requires(!string.IsNullOrEmpty(text)); // 前置條件
29                 Contract.Ensures(Contract.Result<string>() != null); // 后置條件
30                 return default(string);// 如果沒有實現此類，則返回默認值。
31             }
32 
33             private ICaseConverterContracts() { } // 禁止實例化該類
34         }
35 
36         /// <summary>
37         /// 實現類
38         /// </summary>
39         public class CurrentCultrueUpperCaseFormatter : ICaseConverter // 繼承接口中的契約
40         {
41             public string Convert(string text)
42             {
43                 return text.ToUpper(CultureInfo.CurrentCulture); // 實現接口方法。（由二進制重寫器執行檢查）
44             }
45         }

　　　　 • 失敗行為

　　　　　　　　Contract全局失敗事件：Contract.ContractFailed ，可注冊並捕獲所有Contract失敗事件

        Contract.ContractFailed += new EventHandler<ContractFailedEventArgs>(Contract_ContractFailed);

...
        static void Contract_ContractFailed(object sender, ContractFailedEventArgs e)
        {
            Console.WriteLine("{0}:{1},{2}", e.FailureKind, e.Condition, e.Message);
            e.SetHandled();
        }

　　三，靜態檢查

　　 • 意義：在編譯時執行檢查，任何錯誤將在Error List中顯示警告信息和錯誤信息。

        static string DontPassMeNull(string input)
        {
            Contract.Requires(input != null);
            Contract.Ensures(Contract.Result<string>() != null);
            return input;
        }

        static string MightReturnNull() 
        {
            return "Not null really";
        }

        /// <summary>
        /// Error list中顯示警告信息
        /// </summary>
        public static void DoTest() 
        {
            DontPassMeNull("definitely okay"); // 總能通過
            DontPassMeNull(MightReturnNull()); // CodeContracts:requires unproven:input != null 無法證明
            DontPassMeNull(null); // 提示錯誤信息
        }