Кодовые контракты - ForAll - Что поддерживается статической проверкой

Существует много информации о том, что статическая проверка Contract.ForAll ограничена или не поддерживается.

Я много экспериментировал и нашел , он может работать с:

Contract.ForAll(items, i => i != null)
Contract.ForAll(items, p) где p имеет тип Predicate<T>

он не может работать с:

Доступ к полям
Доступ к свойствам
Группа методов (я думаю, что делегат здесь все равно)
вызов метода экземпляра

Мои вопросы:

Каковы другие типы кода, с которыми может работать ForAll?
Договорились ли договоры о кодексе, что после Contract.ForAll(items, i => i != null), что, когда один элемент из списка позже в коде (т.е. путем индексирования), элемент не является нулевым?

Вот полный тестовый код:

public sealed class Test
{
    public bool Field;
    public static Predicate<Test> Predicate;

    [Pure]
    public bool Property
    {
        get { return Field; }
    }    

    [Pure]
    public static bool Method(Test t)
    {
        return t.Field;
    }

    [Pure]
    public bool InstanceMethod()
    {
        return Field;
    }

    public static void Test1()
    {
        var items = new List<Test>();
        Contract.Assume(Contract.ForAll(items, i => i != null));
        Contract.Assert(Contract.ForAll(items, i => i != null)); // OK
    }

    public static void Test2()
    {
        var items = new List<Test>();
        Contract.Assume(Contract.ForAll(items, Predicate));
        Contract.Assert(Contract.ForAll(items, Predicate)); // OK
    }

    public static void Test3()
    {
        var items = new List<Test>();
        Contract.Assume(Contract.ForAll(items, i => i.Field));
        Contract.Assert(Contract.ForAll(items, i => i.Field)); // assert unproven
    }

    public static void Test4()
    {
        var items = new List<Test>();
        Contract.Assume(Contract.ForAll(items, i => i.Property));
        Contract.Assert(Contract.ForAll(items, i => i.Property)); // assert unproven
    }

    public static void Test5()
    {
        var items = new List<Test>();
        Contract.Assume(Contract.ForAll(items, Method));
        Contract.Assert(Contract.ForAll(items, Method)); // assert unproven
    }

    public static void Test6()
    {
        var items = new List<Test>();
        Contract.Assume(Contract.ForAll(items, i => i.InstanceMethod()));
        Contract.Assert(Contract.ForAll(items, i => i.InstanceMethod()));// assert unproven
    }
}

Ответ 1

Мне не удалось найти больше рабочих выражений, на самом деле я обнаружил, что даже Contract.ForAll(items, i => i != null) не работает надежно (но он понимает, что элемент не имеет значения null, когда позже используется внутри foreach в той же функции). Наконец, я отказался от возможности использовать более сложные контракты ForAll со статическим контролером.

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

Для этого необходимы 2 сборки Debug (если у вас их еще нет), Debug и Debug + Static Contracts, сборка Debug имеет условный символ компиляции MYPROJECT_CONTRACTS_RUNTIME. Таким образом, он получает все контракты Contract. и RtContract.. Другие сборки получают только Contract. контракты.

public static class RtContract
{
    [Pure] [ContractAbbreviator] [Conditional("MYPROJECT_CONTRACTS_RUNTIME")]
    public static void Requires(bool condition)
    {
        Contract.Requires(condition);
    }

    [Pure] [ContractAbbreviator] [Conditional("MYPROJECT_CONTRACTS_RUNTIME")]
    public static void Ensures(bool condition)
    {
        Contract.Ensures(condition);
    }

    [Pure] [Conditional("MYPROJECT_CONTRACTS_RUNTIME")]
    public static void Assume(bool condition)
    {
        Contract.Assume(condition);
    }
}

public class Usage
{
   void Test (int x)
   {
        Contract.Requires(x >= 0);  // for static and runtime
        RtContract.Requires(x.IsFibonacci());  // for runtime only
   }
}

Ответ 2

Декомпилируя mscorelib.dll System.Diagnostics.Contracts, мы можем легко увидеть, как построен контракт. ForAll: он принимает коллекцию и предикат.

public static bool ForAll<T>(IEnumerable<T> collection, Predicate<T> predicate)
{
    if (collection == null)
    {
        throw new ArgumentNullException("collection");
    }
    if (predicate == null)
    {
        throw new ArgumentNullException("predicate");
    }
    foreach (T current in collection)
    {
        if (!predicate(current))
        {
            return false;
        }
    }
    return true;
}

Итак, когда вы говорите Contract.ForAll(items, i => i.Field), в этом случае i => i.Field является предикатом

Затем, следуя вашему примеру во всех методах тестирования, мы видим, что вы предоставляете пустой список методу Contract.ForAll, который вернет true, поскольку он никогда не войдет в блок foreach.

Принимая это, если вы добавите элемент в свой список var items = new List<Test>() {new Test()}; и снова запустите тест, он вернет false, поскольку ваш public bool Field; по умолчанию установлен false

Цель контракта. ForAll -

Определяет, существуют ли все элементы в коллекции внутри Функция

Итак, я пришел к выводу, что речь идет не о Contarct.ForAll не может работать с чем-то, но по крайней мере один элемент в вашей коллекции возвращает false или имеет значение null