C#代码合同:什么可以静态证明,什么不可以？

Question

我可能会说我对Code Contracts非常熟悉:我已经阅读并理解了大部分用户手册,并且已经使用了很长一段时间了,但我仍然有疑问.当我搜索SO代码"未经证实的代码合同"时,有很多点击,都在问为什么他们的具体陈述无法被静态证明.虽然我可以做同样的事情并发布我的具体情况(这是顺便说一句:

)

我更愿意理解为什么任何代码合同条件可以或不可以证明.有时我对它能证明的东西印象深刻,有时我......嗯......礼貌地说:绝对没有留下深刻的印象.如果我想了解这一点,我想知道静态检查器使用的机制.我相信我会从经验中学习,但我会在Contract.Assume所有地方喷洒语句以使警告消失,我觉得这不是Code Contracts的意思.谷歌搜索没有帮助我,所以我想问你们你们的经历:你们看到了什么(不明显的)模式？是什么让你看到光明？

Answer 1

您的施工合同不满意.由于您正在引用对象的字段(this.data),因此其他线程可以访问该字段,并且可以在Assume与第一个参数分辨率和第三个参数分辨率之间更改其值.(ei,它们可能是三个完全不同的阵列.)

您应该将数组分配给局部变量,然后在整个方法中使用该变量.然后分析器将知道满足约束,因为没有其他线程能够更改引用.

var localData = this.data;
if (localData == null) return;
byte[] newData = new byte[localData.Length]; // Or whatever the datatype is.
Array.Copy(localData, newData, localData.Length); // Now, this cannot fail.

这增加了不仅满足约束的好处,而且实际上,在许多情况下使代码更加健壮.

我希望这能引导你回答你的问题.我实际上无法直接回答您的问题,因为我无法访问包含静态检查器的Visual Studio版本.(我在VS2008 Pro上.)我的答案是基于我自己对代码的视觉检查得出的结论,并且看起来静态合同检查器使用了类似的技术.我是无耻的!我需要给我一个.:-D

更新:(有很多猜测要遵循)

经过反思,我想我可以很好地猜测哪些可以或不可以证明(即使没有访问静态检查器).如另一个答案所述,静态检查器不进行过程间分析.因此,随着多线程变量访问的迫在眉睫的可能性(如在OP中),静态检查器只能有效地处理局部变量(如下所定义).

"局部变量"是指任何其他线程都无法访问的变量.这将包括在方法中声明的任何变量或作为参数传递的变量,除非参数使用ref或out在匿名方法中捕获变量.

如果局部变量是值类型,则其字段也是局部变量(等等递归).

如果局部变量是引用类型,则只有引用本身 - 而不是其字段 - 可以被视为局部变量.即使在方法中构造的对象也是如此,因为构造函数本身可能泄漏对构造对象的引用(例如,对于用于高速缓存的静态集合).

只要静态检查器不进行任何过程间分析,任何对上述非本地变量的假设都可以随时失效,因此在静态分析中会被忽略.

例外1:由于运行时将字符串和数组称为不可变的,因此只要字符串或数组变量本身是本地的,它们的属性(如Length)就会受到分析.这不包括其他线程可变的数组内容.

例外2:运行时可能知道数组构造函数不泄漏对构造数组的任何引用.因此,在方法体内构造并且不泄漏到方法外部的数组(作为参数传递给另一个方法,分配给非局部变量等)具有也可以被视为局部变量的元素.

这些限制似乎相当繁重,我可以想象几种可以改进的方法,但我不知道做了什么.从理论上讲,这里还有其他一些可以用静态检查器完成的事情.有方便的人应该检查已经完成的工作和没有完成的工作:

• 它可以确定构造函数是否不泄漏对该对象或其字段的任何引用,并将所构造的任何对象的字段视为局部变量.
• 可以对其他方法进行无泄漏分析,以确定在该方法调用之后传递给方法的引用类型是否仍然可以被视为本地.
• 用ThreadStatic或ThreadLocal修饰的变量可以被视为局部变量.
• 可以给出选项以忽略使用反射来修改值的可能性.这将允许引用类型或静态私有只读字段上的私有只读字段被认为是不可变的.此外,启用此选项时,只能在lock(X){ /**/ }构造内访问且未泄露的私有或内部变量X 可被视为局部变量.但是,这些东西实际上会降低静态检查器的可靠性,所以这有点不确定.

另一种可能打开大量新分析的可能性是声明性地将变量和使用它们的方法(以递归方式)分配给特定的唯一线程.这将是该语言的一个重要补充,但它可能是值得的.

Answer 2

简短的回答是静态代码分析器看起来非常有限.例如,它没有检测到

readonly string name = "I'm never null";

作为一个不变的.从我在MSDN论坛上收集的内容来看,它自己分析每个方法(出于性能原因,而不是认为它可能会慢得多),这限制了它在验证代码时的知识.

为了在证明正确性和能够完成工作的学术崇高目标之间取得平衡,我已经使用装饰个别方法(甚至是必要的课程)

[ContractVerification(false)]

而不是撒上许多假设的逻辑.这可能不是使用CC的最佳实践,但它确实提供了一种在不取消选中任何静态检查器选项的情况下消除警告的方法.为了不丢失这些方法的前/后条件检查,我通常添加具有所需条件的存根,然后调用排除的方法来执行实际工作.

我自己对代码契约的评估是,如果您只使用官方框架库并且没有大量遗留代码(例如,在启动新项目时),那就太棒了.还有别的东西,这是一个快乐和痛苦的混合包.