缺少不变量，坏（？）不变量和奇怪的警告 [英] Missing invariant, bad(?) invariant, and an odd warning

问题描述

你好，

我一直在玩CodeContracts，这很酷。我正在一个相当大的代码库上试验它。一些请求和一个问题：

请为BitArray添加一个Count == Length invariant。根据文档的说法是正确的，并且会为我清理一堆警告。之前已经提到的Stream.Read（）的后置条件也是咬我的（应该是offset + count< = buflen而不是<）。

也，ICollection.Add似乎有a"count == oldCount + 1"后置条件就可以了。文档没有说明这一点，对于我的（4.0之前的）集合实现它不是真的，所以这现在在运行时抛出。可以是"count == oldCount ||" count == oldCount + 1"还是什么呢？
我对生成的警告感到困惑。考虑：

类程序{
static void Foo（List< byte []> fs）{
Contract.Requires（fs！= null）;
Contract.Requires（fs.Count> 0）;
Contract.Requires（Contract.ForAll（fs，f => f！= null））;
int l = fs [0] .Length;

这会弹出一个"可能使用空数组"。在最后一行，就在应该告诉它的Require（）之后，它们都不是null。我错过了什么吗？
除此之外，还有比这个论坛更好的发布这类事情的地方吗？类似bugzilla的东西？

谢谢你，
Lodewijk

hello,

I've been playing with CodeContracts, and it's very cool. I'm experimenting with it on a fairly large codebase. some requests and a question:

please add a Count == Length invariant to BitArray. that's correct per the documentation, and would clean up a heap of warnings for me. Stream.Read()'s postcondition that has already been mentioned before is biting me too (should be offset + count <= buflen instead of <).

also, ICollection.Add seems to have a "count == oldCount + 1" postcondition on it. the documentation says nothing of this, and for my (pre-4.0) set implementation it isn't true, so this now throws up at runtime. can it be "count == oldCount || count == oldCount + 1" or something?

and I'm puzzled about a generated warning. consider:

    class Program {
        static void Foo(List<byte[]> fs) {
            Contract.Requires(fs != null);
            Contract.Requires(fs.Count > 0);
            Contract.Requires(Contract.ForAll(fs, f => f != null));
            int l = fs[0].Length;
        }
    }

this pops an "Possible use of a null array" on the last line, right after the Require() that should tell it none of them are null. am I missing something?

also, is there a better venue to post these kinds of things than this forum? something like a bugzilla?

thank you,
Lodewijk

推荐答案

很抱歉迟到的回复。这些都是仍然有效的问题。在下一个版本中，我们将解决其中一些问题：

Sorry for the late reply. These are all issues that are still active. In the next release we will address some of them:

- 较弱的ICollection.Add合同

- weaker ICollection.Add contract

   确保（Count> = Contract.OldValue（Count））;

    Ensures( Count >= Contract.OldValue(Count) );

- BitArray.Length将有一个等于Count的后置条件

- BitArray.Length will have a post condition that it's equal to Count

- 目前正在研究forall支持。我们已经让它适用于数组，原型也适用于枚举器。但它还没有准备好发布。

- The forall support is currently being worked on. We have have it working for arrays and a prototype is working for enumerators too. But it's not quite ready for release.

请继续在这里发帖。您也可以使用microsoft Connect。

Please keep posting here for now. You can also use microsoft Connect.

这篇关于缺少不变量，坏（？）不变量和奇怪的警告的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！