Асинхронные постусловия в библиотеке Code Contracts

На прошлой неделе я выкатил релиз-кандидат новой версии библиотеки Code Contracts (v.1.10-rc1). В этом релизе было поправлено довольно много, а главной «новой» возможностью стала вменяемая реализация асинхронных постусловий.

Для начала стоит напомнить, что такое постусловия вообще, и асинхронные постусловия в частности.

Постусловие метода – это некоторое условие, которое должно быть истинным при успешном завершении метода. Например, постусловие может гарантировать, что возвращаемое значение не будет равно null, что перед завершением метода Start, состояние будет равняться определенному значению (например, Starting) и т.п.

Вот небольшой пример:

public string GetResult()
{
    Contract.Ensures(Contract.Result<string>() != null);
    return string.Empty;
}
 
enum Status { Init, Starting, Started }
private Status _status;
 
public void Start()
{
    Contract.Ensures(_status == Status.Starting);
}

(Обратите внимание, что в отличие от предусловий, постусловия могут ссылаться на закрытое состояние. Это связано с тем, что клиент класса не должен иметь возможности проверить валидность постусловия, это забота самого метода, ну и инструментов, вроде Code Contracts, которые вставляют проверку условий в каждой точке выхода из метода.)

Обычные предусловия предусловия имеют довольно ограниченную применимость в случае асинхронных методов. В случае метода, который возвращает Task или Task<T>, помимо проверки некоторое условия при выходе из методы, бывает очень полезным проверить некоторое условие во время завершения возвращаемой задачи. Именно для этих целей используются «асинхронные постусловия»).

ПРИМЕЧАНИЕ
Обратите внимание, что «асинхронные постусловия» применимы не только к методам, помеченным ключевым словом async, но и к любым методам, которые возвращают Task или Task<T>. Т.е. асинхронные методы применимы к любым методам, которые следуют TAP (Task-based Asynchronous Pattern)!

Давайте посмотрим на пример асинхронного постусловия. В случае асинхронного метода StartAsync, мы можем определить следующие правила:

· После окончания «синхронной» части метода StartAsync мы хотим гарантировать, что состояние будет равно Starting,

· А после окончания асинхронной операции (т.е. после завершения задачи), состояние должно быть Started.

Сделать это можно следующим образом:

private static Status _status = Status.Init;
 
public static async Task<Status> StartAsync()
{
    Contract.Ensures(_status == Status.Starting);
    // Или же можно использовать
    // Contract.Result<Task<Status>>().Result == Status.Started
    Contract.Ensures(Contract.Result<Status>() == Status.Started);
    // Если мы сделаем await до установки состояния в Staring,
    // то постусловие будет нарушено и мы получим ContractException
    _status = Status.Starting;
    await Task.Delay(42);
    _status = Status.Started;
    return _status;
}

Каждый раз, когда ccrewrite встречает в постусловии Contract.Result<T>() или Contract.Result<Task<T>>().Result, то он генерирует следующий код:

private class AsyncClosure
{
    public Task<Status> CheckPost(Task<Status> task)
    {
        if (task.Status == TaskStatus.RanToCompletion)
        {
            __ContractRuntime.Ensures(task.Result == Status.Started);
        }
        return task;
    }
}
 

public static Task<Status> StartAsyncRewritten()
{
    var asyncClosure = new AsyncClosure();
 
    _status = Status.Starting;
 
    // Проверка синхронного постусловия
    __ContractRuntime.Ensures(_status == Status.Starting);
 
    // Здесь генерируется таска с помощью асинхронного конечного автомата
    // и всяческих AsyncMethodBuilder-ов. Нам в данном случае это не интересно!
    Task<Status> task = null;
 
    // Проверка асинхронного постусловия с помощью продолжения
    return task.ContinueWith(asyncClosure.CheckPost,
        TaskContinuationOptions.ExecuteSynchronously).Unwrap<Status>();
}

В случае асинхронных постусловий, ccrewrite генерирует замыкание (класс AsyncClosure), с единственным методом CheckPost, который предназначен для проверки состояния по завершения задачи. (Да, в случае «исключительных» постусловий, т.е. постусловий, которые должны быть выполнены при генерации методом исключения, генерируется очень похожий код, просто проверка осуществляется только в случае, когда завершенная задача завершилась с ошибкой).

Идея реализации состоит в том, что постусловие проверяется в продолжении, которое задается с помощью ContinueWith на задаче, исходно возвращаемой из текущего метода. ContinueWith в этом случае, по сути декорирует исходную задачу и возвращает тот же самый результат, но с генерацией исключения в случае нарушения постусловия. Поскольку метод CheckPost возвращает Task<Status>, то возвращаемое значение метода ContinueWith будет Task<Task<Status>>. Это значит нам нужно воспользоваться трюком метода TaskExtensions.Unwrap и распаковать полученное значение для получения просто Task<Status>.

Теперь, если постусловие будет нарушено, то клиент получит ContractException, а если нет, то он получит исходную задачу, полученную в результате работы асинхронного метода.

ПРИМЕЧАНИЕ
Асинхронные постусловия были полностью переписаны в версии 1.10. Предыдущая версия генерировала совершенно другой код, который приводил к побочным эффектам, когда задача завершалась неудачно! Так что если у вас были проблемы с асинхронными в старых версиях Code Contracts, то не удивляйтесь – там они были реализованы очень криво!

Асинхронные постусловия не имеют особой синтаксической конструкции в библиотеке Code Contracts. Для их использования нужно в постусловии обратиться к свойству Result возвращаемой задачи, или же просто использовать Contract.Result<T>() в случае если метод возвращает Task<T>. Зная это можно сделать небольшой вспомогательный метод, который будет выражать намерения более явным образом, что может быть полезным, когда асинхронное постусловие должно проверять некоторое состояние объекта, и вообще не трогать возвращаемую задачу:

ПРИМЕЧАНИЕ
Да, асинхронные постусловия совершенно невозможно выразить, если метод возвращает Task!

public static async Task<int> StartAsync()
{
    // Синхронное постусловие
    Contract.Ensures(_status == Status.Starting);
    // Асинхронное постусловие
    Contract.Ensures(AsyncPostcondition(_status == Status.Started, Contract.Result<int>()));
 
    _status = Status.Starting;
    await Task.Delay(42);
 
    _status = Status.Started;
    return 42;
}
 
[Pure]
private static bool AsyncPostcondition<T>(bool predicate, T methodResult)
{
    return predicate;
}

Дополнительные ссылки

• CodeContracts на github.com
• Релиз v.1.10 на гитхаб, в котором реализованы нормальные асинхронные постусловия
• Известная проблема с асинхронным постусловием и захватом состояния