Class invariant to ensure a particular data type on a field does not hold

Question

Given the following code:

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;

using System;

public class Program
{
    public int[] ints = new int[1000];

  [ContractInvariantMethod]
  private void ObjectInvariant ()
  {
    Contract.Invariant(ints.GetType() == typeof(int[]));
    Contract.Invariant(ints != null);
  }
}

Why is the invariant ints.GetType() == typeof(int[]) considered to cannot be proven? If I change the invariant to ints.GetType() == ints.GetType() it passes (without any surpise), but why does it fail for typeof(int[]).

Answer 1

Sadly, you can in fact store objects in an int[] that aren't actually an int[]. There are some valid conversions that you would hope wouldn't be valid, but that in fact are. For example, someone could write:

ints = (int[])(object)new uint[5];

and now the type of ints is an unsigned int array, not an int array. That this conversion is valid is unfortunate (that it's valid almost exclusively just causes bugs when it comes up); it's be great if what you posted could be an invariant, but sadly, Contract.Invariant is correct that it's not.