26

我试图在代码合同中演示不变量，我想我会举一个字符串排序列表的例子。它在内部维护一个数组，有用于添加等的备用空间 - 基本上就像List<T>. 当它需要添加一个项目时，它将它插入到数组中，等等。我想我有三个不变量：

  • 计数必须是合理的：非负数并且最多与缓冲区大小一样大
  • 缓冲区未使用部分中的所有内容都应为空
  • 缓冲区已用部分中的每个项目都应至少与之前的项目一样“大”

现在，我尝试以这种方式实现它：

[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));

这有点难看，尽管它确实有效。（这比我之前的尝试要好得多，请注意。）

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

（也在代码合同论坛中作为问题提出。我将自己在这里添加任何相关答案。）

4

3 回答 3

8

从（初步）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));
于 2009-07-30T20:57:18.693 回答
3

（我会接受 Henk 的回答，但我认为值得添加。）

这个问题现在已经在MSDN 论坛上得到了回答，结果是第一种形式预计不会起作用。不变量真的，真的需要是对 的一系列调用Contract.Invariant，仅此而已。

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

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

Contract.Invariant(IsValid);

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

于 2009-07-31T06:29:09.887 回答
1

设计师不是在重新发明轮子吗？

老好人怎么了

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);
}

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

于 2009-08-23T22:36:38.770 回答