我如何断言私有只读数组总是有项目？ [英] How do I assert that a private readonly array always has items?

问题描述

道歉，如果之前已经介绍过，我找不到早期的参考资料。我觉得我错过了什么。鉴于此类：

 public class AlwaysFullArray 
 {
 private static readonly int [] ALWAYS_FULL_ARRAY = new int [] 
 {
 1，
 2，
 3 
}; 
 
 public int GetFirst（）
 {
 return ALWAYS_FULL_ARRAY.First（）; 
} 

静态验证程序生成"需要未经证实的：任何（来源）"对于GetFirst（）。为了尝试解决这个问题，我添加了以下不变量：

 [ContractInvariantMethod] 
 private void ObjectInvariant（）
 {
 Contract.Invariant（ALWAYS_FULL_ARRAY！= null）; 
 Contract.Invariant（ALWAYS_FULL_ARRAY.Any（））; 
} 

验证者然后生成"不变未经证实：ALWAYS_FULL_ARRAY.Any（）"。它还建议添加" Contract.Ensures（1< = System.Linq.Enumerable.Count（ALWAYS_FULL_ARRAY））"到构造函数，但它也无法证明。
另一方面，如果我将类更改为如下所示：

 public class AlwaysFullArray 
 {
 public static readonly int [] ALWAYS_FULL_ARRAY = new int [] 
 {
 1，
 2，
 3 
}; 
 
 public int GetFirst（）
 {
 Contract.Requires（ALWAYS_FULL_ARRAY.Any（））; 
 
返回ALWAYS_FULL_ARRAY.First（）; 
} 
} 

然后所有断言都被证明成功。鉴于我并不想将该数组公开，有没有办法改变原始的断言以使它们可证明？是什么让他们无法改善？

干杯，

Stephen。

编辑：在预感中，我也尝试使数组非静态，但这也不起作用。

解决方案

我看到您已尝试删除 static 关键字;但是，我认为这是主要问题。  AFAIK，静态检查程序不支持针对
静态字段的不变合同。

如果你要使它成为非静态的，那么以下内容不变量应该起作用：

 Contract.Invariant（ALWAYS_FULL_ARRAY！= null）; 
 Contract.Invariant（ALWAYS_FULL_ARRAY.Length> 0）; 

虽然你不应该让它非静态只是为了让静态检查器满意。   我建议使用
SuppressMessageAttribute 来屏蔽相关警告。 您可以通过将-outputwarnmasks开关添加到项目属性中"代码约定"选项卡上的静态检查器选项来获取适当的值。 
编辑：请注意，构建后，屏幕会出现在"输出"窗口中，而不是错误列表中。

- Dave

Apologies if this has been covered before, I couldn't find an earlier reference. I feel like I'm missing something. Given this class:

public class AlwaysFullArray
    {
        private static readonly int[] ALWAYS_FULL_ARRAY = new int[]
                                                              {
                                                                  1,
                                                                  2,
                                                                  3
                                                              };

        public int GetFirst()
        {
            return ALWAYS_FULL_ARRAY.First();
        }

The static verifier generates a "requires unproven: Any(source)" for GetFirst(). To try and resolve this, I added the following invariants:

        [ContractInvariantMethod]
        private void ObjectInvariant()
        {
            Contract.Invariant(ALWAYS_FULL_ARRAY != null);
            Contract.Invariant(ALWAYS_FULL_ARRAY.Any());
        }

The verifier then generates a "invariant unproven: ALWAYS_FULL_ARRAY.Any()". It also alternatively suggests adding "Contract.Ensures(1 <= System.Linq.Enumerable.Count(ALWAYS_FULL_ARRAY))" to the constructor, but it can't prove that either. On the other hand, if I change the class to look like this:

public class AlwaysFullArray
    {
        public static readonly int[] ALWAYS_FULL_ARRAY = new int[]
                                                              {
                                                                  1,
                                                                  2,
                                                                  3
                                                              };

        public int GetFirst()
        {
            Contract.Requires(ALWAYS_FULL_ARRAY.Any());

            return ALWAYS_FULL_ARRAY.First();
        }
    }

Then all assertions are successfully proven. Given that I don't really want to make that array public, is there any way to alter the original asserts to make them provable? And what's making them unprovable?

Cheers,

Stephen.

EDIT : On a hunch, I also tried making the array non-static, but that didn't work either.

解决方案

Hi,

I see that you already tried removing the static keyword; however, I think that's the main problem.  AFAIK, the static checker does not support invariant contracts against static fields.

If you were to make it non-static, then the following invariants should work:

Contract.Invariant(ALWAYS_FULL_ARRAY != null);
Contract.Invariant(ALWAYS_FULL_ARRAY.Length > 0);

Though you shouldn't make it non-static just to make the static checker happy.  I recommend masking related warnings instead by using the SuppressMessageAttribute.  You can get the appropriate values by adding the -outputwarnmasks switch to the static checker options on the Code Contracts tab in your project's properties.  Edit: Note that the masks appear in the Output window after building, not in the Error List.

- Dave

这篇关于我如何断言私有只读数组总是有项目？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！