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

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

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

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

Контракты и удаленный код

Как вы, наверное, знаете, библиотека Code Contracts использует переписывание IL кода для реализации контрактного программирования. Это «архитектурное» решение является вполне логичным, с одной стороны, поскольку позволяет использовать эту библиотеку с любыми языками программирования на платформе .NET. Но, с другой стороны, это приводит к массе проблем, поскольку ccrewrite должен «реверс-инжинирить» IL код в высокоуровневые конструкции и переписывать его специальным образом.

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

Начать ли использовать контракты?

Тут народ на rsdn-е интересуется, а стоит ли пользоваться Code Contracts,  вопрос интересный. Ответ такой вопрос звучит обычно так:“it depends”, но я могу помочь понять, от чего и что depends.

Краткий экскурс в историю контрактов

Сама идея контрактного программирования появилась в 80-х годах в голове Бертрана Мейера и основывалась на матанских выкладках Хоара и других умных дядек.

Заключалась она в следующем: программа сама по себе не является корректной или не корректной, это понятие применимо лишь к паре – (программа, ожидаемое поведение). А поскольку ожидаемое поведение обычно является совершенно непонятным делом, то хочется иметь возможность в кратком и implementation-agnostic виде выразить это самое поведение. Причем сделать это как можно ближе к реализации этого самого поведения.

Для выражения ожидаемого поведения (a.k.a. спецификации) использовались утверждения, а чтобы понять, кто в программе не прав, вызывающий или вызываемый код, то добавлено несколько видов утверждений:

Code Contracts в VS2015

В последние несколько недель я активно занимался доработкой Code Contracts, исправлением некоторых неприятных ошибок и добавлением поддержки VS2015. А поскольку VS2015 только что увидела свет, то подобная поддержка будет весьма кстати. Теперь обо всем об этом по порядку, да еще и с рядом технических подробностей.

Итак, первое, что нужно знать о Code Contracts, что эта штука жива. Код лежит в открытом доступе на гитхабе (https://github.com/Microsoft/CodeContracts) и есть ряд людей, которые активно занимаются наведением там порядка. Я являюсь owner-ом репозитория, но занимаюсь этим в свое свободное время. Помимо меня есть еще несколько человек, которые наводят порядок в Code Contracts Editor Extensions (@sharwell) и в некоторых других областях.

Code Contracts можно разделить на несколько составляющих:

• ccrewrite – тул, который занимается «переписыванием» IL-а, выдиранием утверждений (Contract.Requires/Ensures/Assert/Assume/if-throw) и заменой их на нужные вызовы методов контрактов, в зависимости от конфигурации.
• cccheck - тул, который занимается статическим анализом и формальным доказательством во время компиляции, что программа является корректной.
• Code Contracts Editor Extensions – расширение к VS, которое позволяет «видеть» контракты прямо в IDE.

Есть еще ряд тулов, например, для генерации документации, а также плагин к ReSharper, который упрощает добавление предусловий/постусловий и показывает ошибки ccrewrite прямо в IDE.

Я занимаюсь двумя составляющими – ccrewrite и плагином, но сейчас хочу остановиться именно на ccrewrite и на сложностях, с которыми я столкнуться при добавлении поддержки VS2015.