Asynchronous Post-Conditions in Code Contracts Library

I rolled out the release candidate of the new version of the Code Contracts library last week (v.1.10-rc1). This release has quite a lot of fixes, but the main "new" opportunity is a proper implementation of asynchronous post-conditions.

For starters it is worth recalling what post-conditions, and in particular asynchronous post-conditions, are in general.

A post-condition of a method is a condition that must be true on the successful completion of the method. For example, post-condition can ensure that the returned value is not equal to null, or that before the completion of the Start method the status will be equal to a certain value (e.g., Starting), etc.

Here is a small example:

(Please note that in contrast to the pre-conditions, post-conditions may refer to the closed state. This is due to the fact that the class client should not be able to check the validity of the post-condition; this is a concern of the method itself, and of the tools, such as Code Contracts, which insert condition checks at each point of exit from a method.)

Conventional pre-conditions and post-conditions have a rather limited applicability in the case of asynchronous methods. In the case of a method that returns a Task or Task<T>, in addition to the check of some conditions at the exit from the method, it is sometimes very useful to check some conditions at the time of the completion of the returned task. "Asynchronous post-conditions" are used exactly for this purpose.

NOTE
Note that "asynchronous post-conditions" are applicable not only to the methods marked with the async keyword, but also to any methods that return a Task or Task<T>. I.e. asynchronous methods can be applied to any of the methods that follow TAP (Task-based Asynchronous Pattern)!

Let's look at the example of an asynchronous post-condition. In the case of an asynchronous StartAsync method, we can define the following rules:

After the end of the "synchronous" part of the StartAsync method we want to ensure that the status will be equal to Starting,
And after the end of asynchronous operation (i.e., after the task is completed), the status should be Started.

This can be done as follows:

Whenever ccrewrite meets Contract.Result<T>() or Contract.Result<Task<T>>().Result in the post-condition, it generates the following code:

In the case of asynchronous post-conditions, ccrewrite generates a closure (AsyncClosure class), with the only CheckPost method which is intended to check the status on task completion. (Yes, in the case of "exceptional" post-conditions, i.e. post-conditions that must be fulfilled in the generation by exception, a very similar code is generated, but the check is performed only if the task is completed with errors).

The idea behind it is that a post-condition is checked in the continuation which is defined by ContinueWith at the task, initially returned from the current method. ContinueWith in this case, in fact, decorates the original task and returns the same result, but with the generation of an exception in the case of a violation of the post-condition. Since CheckPost method returns a Task<Status>, the returned value of the method ContinueWith will be Task<Task<Status>>. This means we need to use a trick from the method TaskExtensions.Unwrap and unwrap the resulting value to obtain a simple Task<Status>.

Now, if the post-condition is violated, the client will receive a ContractException, and if not, it will receive the original task obtained as a result of the work of an asynchronous method.

NOTE
Asynchronous post-conditions have been completely rewritten in version 1.10. Previous versions generated a completely different code, which resulted in side effects when a task failed! So if you had problems with asynchronous post-conditions in older versions of Code Contracts, do not be surprised - they were implemented very badly there!

Asynchronous post-conditions do not have special syntax in the Code Contracts library. To use them, you need to refer to the Result property of a returned task in a post-condition, or just use Contract.Result<T>() if the method returns a Task <T>. Knowing this, you can create a small helper method that will express the intentions more clearly, which can be useful when an asynchronous post-condition must check a state of the object without touching the returned task:

NOTE
Yes, it is absolutely impossible to express an asynchronous post-condition if the method returns a Task!

Sergey Teplyakov
Expert in .Net, С++ and Application Architecture