Кодовые контракты и асинхронность

Question

Каков рекомендуемый способ добавления постусловий в асинхронные методы, которые возвращают Task<T>?

Я прочитал следующее предложение:

http://social.msdn.microsoft.com/Forums/hu-HU/async/thread/52fc521c-473e-4bb2-a666-6c97a4dd3a39

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

1. Асинхронный метод, хотя предполагается, что он является оберткой для метода синхронизации, остается без какого-либо контракта с реальным кодом и поэтому может выполнять все, что пожелает.
2. Кодовые базы, которые привержены асинхронности, вряд ли будут реализовывать аналоги синхронизации для всего. В результате реализация новых методов, которые содержат await s в других асинхронных методах, следовательно, вынуждена быть асинхронной. Эти методы изначально асинхронны и не могут быть легко преобразованы в синхронные. Они не просто фантики.

Даже если бы мы опровергли последний пункт, сказав, что мы можем использовать .Result или .Wait() вместо await (что фактически приведет к тупику некоторых SyncContext, и его придется переписать в любом случае асинхронный метод), я все еще убежден в первом пункте.

Есть ли альтернативные идеи, или я что-то упустил из-за контрактов с кодом и TPL?

Answer 1

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

Я не рекомендую писать асинхронные методы как оболочки для методов синхронизации. На самом деле, я бы хотел поступить наоборот.

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

Постусловия в значительной степени нарушены.

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

Инварианты не имеют особого смысла в мире Async, где изменчивое состояние имеет тенденцию просто мешать. (Async мягко отталкивает вас от ООП к функциональному стилю).

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

В то же время вы можете создать притворное условие, написав предположение:

// Synchronous version for comparison.
public static string Reverse(string s)
{
  Contract.Requires(s != null);
  Contract.Ensures(Contract.Result<string>() != null);

  return ...;
}

// First wrapper takes care of preconditions (synchronously).
public static Task<string> ReverseAsync(string s)
{
  Contract.Requires(s != null);

  return ReverseWithPostconditionAsync(s);
}

// Second wrapper takes care of postconditions (asynchronously).
private static async Task<string> ReverseWithPostconditionAsync(string s)
{
  var result = await ReverseImplAsync(s);

  // Check our "postcondition"
  Contract.Assume(result != null);

  return result;
}

private static async Task<string> ReverseImplAsync(string s)
{
  return ...;
}

Некоторое использование контрактов кода просто невозможно - например, указание постусловий для асинхронных членов интерфейсов или базовых классов.

Лично я только что полностью избежал контрактов в своем асинхронном коде, надеясь, что Microsoft исправит это через несколько месяцев.

Answer 2

Напечатал это, но забыл нажать "Post" ...:)

В настоящее время нет специальной поддержки для этого.Лучшее, что вы можете сделать, это что-то вроде этого (без использования ключевого слова async, но с той же идеей - возможно, перезаписывающее устройство будет работать по-другому при асинхронной CTP, я еще не пробовал):

public static Task<int> Do()
{
    Contract.Ensures(Contract.Result<Task<int>>() != null);
    Contract.Ensures(Contract.Result<Task<int>>().Result > 0);

    return Task.Factory.StartNew(() => { Thread.Sleep(3000); return 2; });
}

public static void Main(string[] args)
{
    var x = Do();
    Console.WriteLine("processing");
    Console.WriteLine(x.Result);
}

Однако это означает, что метод «асинхронный» фактически не вернется, пока не завершится оценка Задачи, поэтому «обработка» не будет напечатана, пока не истечет 3 секунды.Это похоже на проблему с методами, которые лениво возвращают IEnumerable s - Контракт должен перечислить все элементы в IEnumerable, чтобы убедиться, что условие выполняется, даже если вызывающая сторона фактически не использует все элементы.

Вы можете обойти это, изменив режим контрактов на Preconditions, но это означает, что никакие постусловия на самом деле не будут проверяться.

Статическая проверка также не может подключить Resultс лямбдой, так что вы получите сообщение «Гарантирует недоказанность».(В общем, статическая проверка в любом случае ничего не доказывает о лямбдах / делегатах.)

Я думаю, чтобы получить надлежащую поддержку Задач / ожидать, команде Code Contracts придется добавить в Задачи особый случай, чтобы добавить предварительное условие.проверять только при доступе к полю Result.

Answer 3

Публикация нового ответа на эту старую ветку, так как он возвращается Google в качестве первого ответа на вопрос о CodeContract и Async

На данный момент контракт на возврат асинхронных методов Task работает корректно, и избегать их не нужно.

Стандартный контракт для асинхронного метода:

[ContractClass(typeof(ContractClassForIFoo))]
public interface IFoo
{
    Task<object> MethodAsync();
}


[ContractClassFor(typeof(IFoo))]
internal abstract class ContractClassForIFoo : IFoo
{
    #region Implementation of IFoo

    public Task<object> MethodAsync()
    {
        Contract.Ensures(Contract.Result<Task<object>>() != null);
        Contract.Ensures(Contract.Result<Task<object>>().Status != TaskStatus.Created);
        Contract.Ensures(Contract.Result<object>() != null);
        throw new NotImplementedException();
    }

    #endregion
}

public class Foo : IFoo
{
    public async Task<object> MethodAsync()
    {
        var result = await Task.FromResult(new object());
        return result;
    }
}

Если вы считаете, что контракт выглядит некорректно, я согласен, что он, по крайней мере, вводит в заблуждение, но он работает. И это не похоже на то, что переписчик контракта заставляет оценивать задачу преждевременно.

Когда Стивен высказал некоторые сомнения, я провел еще несколько тестов, и контракты в моем случае сделали свое дело правильно.

Код, использованный для тестирования:

public static class ContractsAbbreviators
{
    [ContractAbbreviator]
    public static void EnsureTaskIsStarted()
    {
        Contract.Ensures(Contract.Result<Task>() != null);
        Contract.Ensures(Contract.Result<Task>().Status != TaskStatus.Created);
    }

}

[ContractClass(typeof(ContractClassForIFoo))]
public interface IFoo
{
    Task<int> MethodAsync(int val);
}

[ContractClassFor(typeof(IFoo))]
internal abstract class ContractClassForIFoo : IFoo
{
    public Task<int> MethodAsync(int val)
    {
        Contract.Requires(val >= 0);
        ContractsAbbreviators.EnsureTaskIsStarted();
        Contract.Ensures(Contract.Result<int>() == val);
        Contract.Ensures(Contract.Result<int>() >= 5);
        Contract.Ensures(Contract.Result<int>() < 10);
        throw new NotImplementedException();
    }
}

public class FooContractFailTask : IFoo
{
    public Task<int> MethodAsync(int val)
    {
        return new Task<int>(() => val);
        // esnure raises exception // Contract.Ensures(Contract.Result<Task>().Status != TaskStatus.Created); 
    }
}

public class FooContractFailTaskResult : IFoo
{
    public async Task<int> MethodAsync(int val)
    {
        await Task.Delay(val).ConfigureAwait(false);
        return val + 1;
        // esnure raises exception // Contract.Ensures(Contract.Result<int>() == val);
    }
}

public class Foo : IFoo
{
    public async Task<int> MethodAsync(int val)
    {
        const int maxDeapth = 9;

        await Task.Delay(val).ConfigureAwait(false);

        if (val < maxDeapth)
        {
            await MethodAsync(val + 1).ConfigureAwait(false);
        }

        return val;
    }
}