How do I assert that a private readonly array always has items?

Question

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.

Answer 1

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

---

http://davesexton.com/blog

Answer 2

Which version are you using?  With the latest version (1.4.51019.0) I don't get any suggestions or warnings with the following:

class NonEmptyArrayTest
{
    private static readonly int[] NonEmptyArray = new [] {1, 2, 3, 4};

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

If I enable "Suggest Ensures" I get two post condition suggestions, but no warnings.

Answer 3

I think you should either add the object invariant, or use the infer object invariants option.

ciao

f

Answer 4

Hi Jesse,

I'm using the same version as you, and your code compiles in my VS with one warning: requires unproven: Any(source). Perhaps we're using different options? My warning level is set to "high", which I think in this case is appropriate?

Cheers,

Stephen.

Answer 5

Hi Dave,

Is this what you're thinking of?

using System.Diagnostics.Contracts;
using System.Linq;


namespace ContractTest
{
    public class AlwaysFullArray
    {
        [ContractInvariantMethod]
        private void ObjectInvariant()
        {
            Contract.Invariant(ALWAYS_FULL_ARRAY != null);
            Contract.Invariant(ALWAYS_FULL_ARRAY.Length > 0);
        }

        private readonly int[] ALWAYS_FULL_ARRAY = new int[]
                                                              {
                                                                  1,
                                                                  2,
                                                                  3
                                                              };

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

This still generates the warning. And if I substitute a .Any() check instead of the Length check, the verifier instead complains of not being able to prove the invariant.

Answer 6

Hi,

Yes, that's what I was thinking.  I don't know why you're still getting the warning.

Did you try enabling the Infer Invariants setting as suggested by Francesco?

- Dave

---

http://davesexton.com/blog

Answer 7

Hi Dave,

Yes, I've tried enabling Infer Invariants, but no joy.

Cheers,

Stephen.