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

Question

我试图演示代码契约中的不变量，并且我想我应该给出一个排序的字符串列表的示例。 它在内部维护一个数组，并具有用于添加等的备用空间 - 基本上就像 List 一样。 当它需要添加一个项目时，它将其插入到数组中，等等。我认为我有三个不变量：

• 计数必须合理：非负且最多与缓冲区大小一样大
• 缓冲区的未使用部分中的所有内容应该为 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));

Answer 2

（我将接受 Henk 的回答，但我认为值得添加这一点。）

该问题现已在 MSDN 论坛，结果是第一个表单无法工作。 不变量确实需要是一系列对 Contract.Invariant 的调用，仅此而已。

这使得静态检查器更容易理解不变量并强制执行它。

可以通过简单地将所有逻辑放入不同的成员（例如 IsValid 属性），然后调用来规避此限制：

Contract.Invariant(IsValid);

这无疑会弄乱静态检查器，但在某些情况下，它可能是一个在某些情况下有用的替代方案。

Answer 3

设计师是不是有点重新发明轮子了？

好旧的出了什么问题

bool Invariant() const; // in C++, mimicking Eiffel

？

现在在 C# 中我们没有 const，但是为什么不能定义一个 Invariant 函数

private bool Invariant()
{
  // All the logic, function returns true if object is valid i.e. function
  // simply will never return false, in the absence of a bug
}
// Good old invariant in C#, no special attributes, just a function

，然后根据该函数使用代码契约呢？

[ContractInvariantMethod]
private void ObjectInvariant()
{
    Contract.Invariant(Invariant() == true);
}

也许我写的是废话，但即使在这种情况下，当每个人都告诉我错误时，它也会有一些说教价值。