Кодови договори и асинхронност

Посочих това на екипа на Async, както други направиха. Понастоящем договорите и Async са (почти) взаимно изключващи се. Така че поне някои хора в Microsoft са наясно с проблема, но не знам какво планират да направят по въпроса.

Не препоръчвам писането на асинхронни методи като обвивки за синхронизиращи методи. Всъщност бих склонил да направя обратното.

Предварителните условия могат да работят. Не съм го пробвал скоро; може да се нуждаете от малка обвивка около вашия асинхронен метод, която включва предварителните условия.

Постусловията са доста нарушени.

Твърденията и предположенията работят нормално, но статичната проверка е наистина ограничена, защото постусловията са нарушени.

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

Надяваме се, че във VS vNext договорите ще бъдат актуализирани с асинхронен вид постусловие, което също би позволило на статичната проверка да работи по-добре с твърдения в асинхронни методи.

Междувременно можете да имате pretend-postcondition, като напишете предположение:

// 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 ...;
}

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

Лично аз току-що избегнах изцяло договорите в моя Async код, надявайки се, че Microsoft ще го поправи след няколко месеца.

Написах това, но забравих да натисна "Публикуване"... :)

В момента няма специализирана поддръжка за това. Най-доброто, което можете да направите, е нещо подобно (без използване на ключова дума 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);
}

Това обаче означава, че методът „async“ всъщност няма да се върне, докато Задачата не завърши оценката, така че „обработката“ няма да бъде отпечатана, докато не изтекат 3 секунди. Това е подобно на проблема с методите, които лениво връщат IEnumerables, договорът трябва да изброи всички елементи в IEnumerable, за да гарантира, че условието е изпълнено, дори ако повикващият всъщност няма да използва всички елементи.

Можете да заобиколите това, като промените режима на вашите договори на Preconditions, но това означава, че никакви постусловия всъщност няма да бъдат проверени.

Статичната проверка също не може да свърже Result с ламбда, така че ще получите съобщение „Гарантира недоказано“. (По принцип статичната проверка така или иначе не доказва неща за ламбда/делегати.)

Мисля, че за да получи подходяща поддръжка за Tasks/await, екипът на Code Contracts ще трябва да добави специални случаи Tasks, за да добави проверката на предварителното условие само при достъп до полето Result.

Публикуване на нов отговор в тази стара тема, тъй като е върнат от google като първи отговор на въпрос относно CodeContract и Async

В момента Contract on 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;
    }
}