我在对象不变的代码中有多自由？

Question

我试图在代码契约中展示不变量,我想我会给出一个排序的字符串列表的例子.它在内部维护一个数组,有额外的空间用于添加等 - 就像List<T>基本上一样.当它需要添加一个项目时,它会将它插入到数组中,等等.我想我有三个不变量:

• 计数必须合理:非负数,最多与缓冲区大小一样大
• 缓冲区未使用部分中的所有内容都应为null
• 缓冲区的已使用部分中的每个项目应至少与其前面的项目一样"大"

现在,我试图以这种方式实现它:

[ContractInvariantMethod]
private void ObjectInvariant()
{
    Contract.Invariant(count >= 0 && count <= buffer.Length);
    for (int i = count; i < buffer.Length; i++)
    {
        Contract.Invariant(buffer[i] == null);
    }
    for (int i = 1; i < count; i++)
    {
        Contract.Invariant(string.Compare(buffer[i], buffer[i - 1]) >= 0);
    }
}

不幸的是,ccrewrite搞乱了循环.

用户文档说该方法应该是一系列调用Contract.Invariant.我是否真的必须像这样重写代码？

Contract.Invariant(count >= 0 && count <= buffer.Length);
Contract.Invariant(Contract.ForAll
    (count, buffer.Length, i => buffer[i] == null));
Contract.Invariant(Contract.ForAll
    (1, count, i => string.Compare(buffer[i], buffer[i - 1]) >= 0));

这有点难看,虽然它确实有效.(请注意,这比我以前的尝试要好得多.)

我的期望是不合理的吗？我的不变量是不合理的吗？

(也是代码合同论坛中的一个问题.我会在这里添加任何相关的答案.)

Answer 1

从(初步)MSDN页面看起来,Contract.ForAll成员可以帮助您完成2个范围的合同.但是文档对其功能并不十分清楚.

//untested
Contract.Invariant(Contract.ForAll(count, buffer.Length, i => buffer[i] == null));
Contract.Invariant(Contract.ForAll(1, count, 
    i => string.Compare(buffer[i], buffer[i - 1]) >= 0));