后置条件和对象固定-白红宇

后置条件

后置条件用Contract.Ensures()方法判断，是在方法结束后作验证。如果本方法对方法参数作验证，只对参数的传入时的值进行验证，所以本方法一般情况下是对类中的字段作验证。

对于异常处理，有一个Contract.EnsuresOnThrow()方法，这个方法是当代码抛出异常时，并且不后置条件为false时触发。

在方法的内部，可以用Contract.Result<T>来得到本方法的返回值，T是返回值类型，如果方法返回值是void，则不能使用Contract.Result方法，举例如下：

public double SetAge(int age)

{

Contract.Ensures(Contract.Result<double>() > 10.0);

return 10.0;

}

Contract.OldValue(字段)，在方法内能访问到的参数和字段都可以用这个方法取到初始值。但有一些情况例外：

1、如果一个引有类型没有被初始化，代码如下：

string s;

public double SetAge(int age, bool bol)

{

Console.WriteLine(Contract.OldValue(s.Length ));

return 0;

}

2、因为out参数没有值，不能在Contract.OldValue()方法中得到出参的

如果方法有out参数，可以用Contract.valueAtReturn，来作后置条件。

public void SetAge(out int abc)

{

Contract.Ensures(Contract.ValueAtReturn(out abc)<150&&Contract.ValueAtReturn(out abc)>0);

abc = 30;

}

对象固定

对象固定，就是为了对象业务逻辑的完整性，合用下面方法对对象内部的字段作有效性验证。本例验证在对象被实例化时，age字段的取值范围。

[ ContractInvariantMethod]

void ObjectValidate()

{

Contract.Invariant(this.age > 0 && this.age < 150);

}

这个方面是的协定在方法体里验证，并且本方法是私用，并且加Contractinvariantmehtod的属性（Attribute）

本文转自桂素伟51CTO博客，原文链接： http://blog.51cto.com/axzxs/500968，如需转载请自行联系原作者