如何为现有框架(BCL)代码指定代码合同？

Question

代码合同很有效,直到您必须为Contract.Assume(...)框架代码中的结果添加一个bazillion .例如,MemoryStream.ToArray()永远不会返回一个空数组,就像我在Reflector中查看它一样,但它没有记录为契约,所以我必须Assume到处都是.

是否有一种神奇的方法来为已经存在的功能创建合同库？我猜测,一旦你完成了几十个最常用的框架功能,这些警告就会变得更加可口.

Answer 1

我认为你不能直接。有几件事要做：

请求将合同添加到代码合同论坛的此线程中。

代码契约团队目前建议的解决方法是创建一个静态方法来假设您需要的所有契约。我发现这最适合使用扩展方法：

static class Contracted
{
    byte[] ToArrayContracted(this MemoryStream s)
    {
        Contract.Requires(s != null);
        Contract.Ensures(Contract.Result<byte[]>() != null);

        var result = s.ToArray();
        Contract.Assume(result != null);
        return result;
    }
}

这样，您可以使用s.ToArrayContracted()代替s.ToArray()，一旦合同在该类型上可用，您就可以搜索并替换ToArrayContracted为ToArray。