《C#高级编程》读书笔记（十四）：代码协定

一，代码协定

    代码协定通常称作契约式编程，包括如下三个部分：

1. 前置条件（precondiction）：为了调用函数，必须为真的条件，在其违反时，函数决不调用，传递好数据是调用者的责任。
2. 后置条件（postcondion）：函数保证能做到的事情，函数完成时的状态，函数有这一事实表示它会结束，不会无休止的循环
3. 类不变项（class invariant）：从调用者的角度来看，该条件总是为真，在函数的内部处理过程中，不变项可以为变，但在函数结束后，控制返回调用者时，不变项必须为真。

二，安装插件

    要使用代码协定，首先需要安装Code Contracts for .NET插件。

    安装插件后，可以在项目的属性页中的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表示不执行代码协定检查，即不进行代码协定注入。

三，前置条件

    前置条件检查传递给方法的参数。使用Contract类中的Requires()方法可以定义前置条件。

public static void MinMax(int min, int max)
        {
            Contract.Requires(max>min);
            //...
        }

    调用：

MinMax(1,1);

   因为不满足前置条件，会报出异常：

    Require()方法的重载方法：

public static void Requires(bool condition);
public static void Requires(bool condition, string userMessage);
public static void Requires<TException>(bool condition) where TException : Exception;
public static void Requires<TException>(bool condition, string userMessage) where TException : Exception;

    例如，使用Requires方法的泛型变体可以指定当条件不满足时，调用的异常类型。如果参数o为空，下面的协定就抛出一个ArgumentNullException异常：

        public static void Preconditions(object o)
        {
            Contract.Requires<ArgumentNullException>(o!=null,"Preconditions,o may not be null");
        }

    为了检测用作参数的集合，Contract类提供了Exists()和ForAll()方法。ForAll()方法检测集合中的没一项，看看他们是否满足条件。

public static void ArrayTest(int[] data)
        {
            Contract.Requires(Contract.ForAll(data,i=>i<12));
        }

四，后置条件

    后置条件定义了方法执行完后共享数据和返回值的保证。尽管后置条件定义了关于返回值的一些保证，但他们必须放在方法的开头；所有的协定要求都必须放在方法的开头。

        static void PostCondition()
        {
            Contract.Ensures(sharedState<6);
            sharedState = 9;
            Console.WriteLine($"change sharedState invariant {sharedState}");
            sharedState = 3;
            Console.WriteLine($"before returing change it to a valid value {sharedState}");
        }

    Ensures()方法的重载方法：

public static void Ensures(bool condition);
public static void Ensures(bool condition, string userMessage);

    为了保证返回某个值，可以对Ensures()方法的协定使用特定的值Result<T>

static int ReturnValue()
        {
            Contract.Ensures(Contract.Result<int>()<6);
            return 3;
        }

    还可以比较新旧值。为此应使用OldValue<T>()方法，它返回在方法入口给变量传递的初始值。

        static int ReturnLargerThanInput(int x)
        {
            Contract.Ensures(Contract.Result<int>()>Contract.OldValue<int>(x));
            return x + 3;
        }

五，类不变项

    不变量为对象生命周期中的变量定义了协定。Contract.Requires()方法定义了输入要求，Contract.Ensures()方法定义了方法结束时的要求。Contract.Invariant()方法定义了在对象整个生命周期中都必须满足的条件。对Contract.Invariant的调用只能放在应用了ContractInvariantMethod特性的方法内。

        private int x = 5;
        [ContractInvariantMethod]
        public void ObjectInvariant()
        {
            Contract.Invariant(x>5);
        }

部分内容参考了：代码协定（一）——简介