CodeContracts 中的前提条件和后置条件

Question

如果我写

 [Pure]
 static string s10 {get;set;}

 static void Main(string[] args)
 {
     Contract.Ensures(s10.Length <= 10); //Contract fails
     s10 = ";uhlakushdflausgdflasgdfljgaskdjgfasd";
 }

因为我没有 VS 的高级版，所以没有静态检查，运行程序后 VS 报告我的问题： Postcondition failed: s10.Length <= 10，很好。

如果我写，

 [Pure]
 static string s10 {get;set;}

 static void Main(string[] args)
 {
    Contract.Requires(s10.Length <= 10); //NullReferenceException
    s10 = ";uhlakushdflausgdflasgdfljgaskdjgfasd";
 }

VS 会报告空引用异常。

这实际上是否意味着，由于 Ensures 是后置条件指令，即使我将其调用作为方法的第一行，它也会像最后一行一样在退出函数之前进行验证吗？

Answer 1

是的 - 代码契约重写器将代码以及其他一些内容移动到适当的位置。值得查看 Reflector 中的结果以了解发生了什么。

我强烈建议您仔细阅读代码契约附带的用户指南。据我所知，这是一份很棒的文档。