Статически проверили дизайн по контракту

Question

Недавно я погорячился идея статический проверить дизайн по контракту в .net 4.0/Visual Studio 2010.

Однако я был опечален, чтобы узнать, что он будет доступен только в Visual Studio Командная система. http://msdn.microsoft.com/en-us/devlabs/dd491992.aspx

Есть ли альтернативы, которые дают статически проверенный дизайн по контракту на C#?

Будет ли монопроект добавлять эту функциональность к компилятору?

Answer 1

Он имеет в виду теоретическое доказательство.

Нет ничего, что помешало бы открытому или коммерческому сообществу реализовать свои собственные. Классы контрактов являются частью BCL и тривиально легко добавлять, скажем, к Mono. «Мы должны будем сделать доказательство теоремы, если мы хотим статически проверять вещи.

Проник не является частью компилятора. Он в основном работает следующим образом:

• Скомпилировать версию двоичного файла с CONTRACTS_FULL. Это испускает все атрибуты Контракта и вызовы статическим методам класса Contract.
• Загрузите сборку «только для отражения» и проанализируйте все байтовые коды метода. Подробный анализ потока с информацией о состоянии позволит показать определенные контракты «всегда верно». Некоторые из них будут «известны в какой-то момент». Другие будут «неспособны статически доказать контракт».

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

Редактировать: Человек, если отражатель был открыт, это было бы здорово для этого. Реализация первого прохода, безусловно, может работать как плагин. Таким образом, логика проверки может быть сконструирована, не беспокоясь о том, как загружаются двоичные файлы. Как только он окажется функциональным (получите его?), Логика может быть извлечена и построена для работы с деревьями синтаксиса, создаваемыми другим загрузчиком сборок (который является открытым исходным кодом). Важная/новая вещь здесь - логика проверки - загрузчик сборок был сделан несколько раз, и ничто не изменилось эффектно для этого использования.

Answer 2

Контракты кода не требуют компилятора C#, поскольку они реализованы как классы в .NET Framework 4.0. Любой компилятор .NET, который может испускать управляемую сборку, можно использовать, хотя C++/CLI, скорее всего, выпустит несовместимую сборку при смешивании управляемого и собственного кода.

В среде IDE имеются дополнительные инструменты для перезаписи полученного ИЛ, чтобы контракты отображались в правильном месте, и, таким образом, авторам проекта Mono необходимо было написать аналогичные инструменты для контрактов для работы на платформе Mono.

Для получения дополнительной информации см. this post.