C# Contract诊断

命名空间 : using System.Diagnostics.Contracts;

属性标记 : [ContractOption(category: "runtime", setting: "checking", enabled: true)]

事件订阅 : Contract.ContractFailed += (sender, e) => {  Console.WriteLine(e.Message);  };

 1、 Requires() 定义前提条件

static void MinMax(int min,int max)
        {
            Contract.Requires(min <= max);
            Contract.Requires <ArgumentException>(min <= max);
        }
        static void Preconditions(object o)
        {
            Contract.Requires<ArgumentNullException>(o != null, "Preconditions, o may not be null");
            Console.WriteLine(o.GetType().Name);
        }
        static void ArrayTest(int [] data)
        {
            Contract.Requires(Contract.ForAll(data, i => i < 12));
            Console.WriteLine("ArrayTest contract succeeded");
        }
        public void ArrayTestWithPureMethod(int [] data)
        {
            Contract.Requires(Contract.ForAll(data, MyDataCheck));
            Console.WriteLine("ArrayWithPureMethod succeeded");
        }

        public int MaxVal { get; set; }
        public bool MyDataCheck(int x)
        {
            return x <= MaxVal;
        }

2、  Ensures() 定义后置条件

  private static int sharedState = 5;

        static void Postcondition()
        {
            Contract.Ensures(sharedState < 6);
            sharedState = 9;
            Console.WriteLine("change sharedState invariant {0}", sharedState);
            sharedState = 3;
            Console.WriteLine("before returning change it to a valid value {0}", sharedState);
        }

        static int ReturnValue()
        {
            Contract.Ensures(Contract.Result<int>() < 6);
            return 3;
        }
        static int ReturnLargerThanInput(int x)
        {
            Contract.Ensures(Contract.Result<int>() > Contract.OldValue<int>(x));
            return x+3;
        }
        static void OutParameters(out int x, out int y)
        {
            Contract.Ensures(Contract.ValueAtReturn<int>(out x) > 5 && Contract.ValueAtReturn<int>(out x) < 20);
            Contract.Ensures(Contract.ValueAtReturn<int>(out y) % 5 == 0);
            x = 8;
            y = 10;
        }

3、  Invariant() 定义在对象的整个生命周期中都必须满足的条件

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

        public void Invariant()
        {
            x = 3;
            Console.WriteLine("invariant value: {0}", x);
        }

4、  Pure特性，可以把方法和类型标记为纯粹的方法，纯粹指的是自定义方法不会修改对象的任何可见状态。

5、  接口协定

[ContractClass(typeof(PersonContract))]
   public  interface IPerson
    {
       string FirstName{get;set;}
       string LastName { get; set; }
       int Age { get; set; }
       void ChangeName(string firstName, string lastName);
    }

 [ContractClassFor(typeof(IPerson))]
   public abstract class PersonContract:IPerson
    {
         string IPerson.FirstName
        {
            get
            {
                return Contract.Result<string>();
            }
            set
            {
                Contract.Requires(value != null);
            }
        }

         string IPerson.LastName
        {
            get
            {
                return Contract.Result<string>();
            }
            set
            {
                Contract.Requires(value != null);
            }
        }

         int IPerson.Age
        {
            get
            {
                Contract.Ensures(Contract.Result<int>() >= 0 && Contract.Result<int>() < 121);
                return Contract.Result<int>();
            }
            set
            {
                Contract.Requires(value >= 0 && value < 121);
            }
        }

          void IPerson.ChangeName(string firstName, string lastName)
        {
            Contract.Requires(firstName != null);
            Contract.Requires(lastName != null);
        }
    }


 public  class Person:IPerson
    {
      public Person() { }
      public Person(string firstName,string lastName)
      {
          this.FirstName = firstName;
          this.LastName = lastName;
      }
        public string FirstName
        {
            get ;
             set;
         
        }

        public string LastName
        {
            get;
             set;
        }

        public int Age
        {
            get;
             set;
        }

        public void ChangeName(string firstName, string lastName)
        {
            this.FirstName = firstName;
            this.LastName = lastName;
        }
    }