Инвариант класса для обеспечения того, чтобы определенный тип данных в поле не содержал

Question

Учитывая следующий код:

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

Почему инвариант ints.GetType() == typeof(int[]) считается не может быть доказано? Если я изменю инвариант на ints.GetType() == ints.GetType() это проходит (без каких-либо сюрпризов), но почему это терпит неудачу для typeof(int[]),

Answer 1

К сожалению, вы можете хранить объекты в int[] которые на самом деле не int[], Есть некоторые действительные преобразования, которые, как вы надеетесь, не будут действительными, но на самом деле это так. Например, кто-то может написать:

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

а теперь тип ints это массив int без знака, а не массив int. Это преобразование действительно неудачно (что оно действительно почти исключительно вызывает ошибки, когда оно возникает); было бы здорово, если бы то, что вы опубликовали, могло быть инвариантом, но, к сожалению, Contract.Invariant правильно, что это не так.