Что нужно для доказательства этого Контракта. Требует?

Question

У меня есть приложение, которое проходит раунды в турнире, и я получаю предупреждение о контракте по этой упрощенной структуре кода:

    public static void LoadState(IList<Object> stuff)
    {
        for(int i = 0; i < stuff.Count; i++)
        {
            // Contract.Assert(i < stuff.Count);
            // Contract.Assume(i < stuff.Count);

            Object thing = stuff[i];

            Console.WriteLine(thing.ToString());
        }
    }

Предупреждение:

contracts: requires unproven: index < @this.Count

Что я делаю не так? Как я могу доказать это на IList<T>? Это ошибка в статическом анализаторе? Как мне отправить отчет об ошибке в Microsoft?

Answer 1

Это выглядит странно. К сожалению, я использую Pro версию VS2010 с Code Contracts, поэтому я не могу сам запустить cccheck, чтобы поиграть.

Вам определенно нужен индекс, а не просто использование цикла foreach?

Просто чтобы быть уверенным - ваш упрощенный пример выше выдает ту же ошибку? Всегда стоит проверить, что упрощение не устранило проблему :) Например, вы делаете что-то еще для stuff, которое контролер контрактов может использовать для аннулирования гарантии о stuff.Count?

Answer 2

Я проверил это с помощью версий кода контрактов 1.2.21023.14 и не получил предупреждений. Я предполагаю, что это ошибка, которая с тех пор была исправлена.