代码之家 › 专栏 › 技术社区 › Jon Skeet

在对象不变量的代码中我能有多自由?

invariants visual-studio-2010-beta-1 code-contracts .net-4.0

25

Jon Skeet · 技术社区 · 16 年前

我试图演示代码契约中的不变量,我想我应该给出一个字符串排序列表的示例。它在内部维护一个阵列,并为添加等预留空间-就像 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));

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

(也被作为一个 question in the Code Contracts forum

3 回复 | 直到 16 年前

1

8

user541686 14 年前

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

2

3

Jon Skeet 16 年前

(我将接受亨克的回答,但我认为值得补充这一点。)

这个问题现在已在会议上得到答复 MSDN forum ,结果是第一种形式 不是吗 我希望能工作。不变量真的,真的需要一系列调用 Contract.Invariant ,仅此而已。

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

只需将所有逻辑放在不同的成员(例如 IsValid 属性,然后调用:

Contract.Invariant(IsValid);

3

1

Daniel Daranas 16 年前

设计师们不是在重新设计轮子吗?

这辆车怎么了 good old

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

?

现在在C中,我们没有常数,但是为什么不能定义一个 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);
}

也许我在胡说八道,但即使在这种情况下,当每个人都告诉我错了的时候,它也有一定的教育价值。