Статически проверенный дизайн контракта
Craig Larman Применение UML и Шаблонов . В то время как Банда Четырех книг Шаблоны разработки очень поучительна, я нашел, что не "добирался", как использовать шаблоны разработки, пока я не натыкался на книгу Larman в классе программирования.
2 ответа
Он имеет в виду средство доказательства теорем.
Ничего не мешает. сообществу разработчиков ПО с открытым исходным кодом или коммерческому сообществу от реализации собственных. Классы Contracts являются частью BCL, и их легко добавить, скажем, в Mono. «Нам» нужно будет создать средство доказательства теорем, если мы хотим что-то статически проверять.
Программа доказательства не является частью компилятора. В основном это работает следующим образом:
- Скомпилировать версию двоичного файла с определенным
CONTRACTS_FULL. Это испускает все атрибуты Contract и вызывает статические методы классаContract. - Загрузите сборку «только для отражения» и проанализируйте весь байтовый код метода. Подробный анализ потока с информацией о состоянии позволит показать определенные контракты «всегда верными». Некоторые из них станут «известными ложными в какой-то момент». Другие будут «неспособны статически доказать контракт».
По мере того, как инструмент становится лучше, он переходит от выдачи предупреждений о каждом контракте к, в конечном итоге, предоставлению результатов, аналогичных доказательству версии Microsoft.
Редактировать: Человек, если Reflector был с открытым исходным кодом, это было бы здорово для этого. Реализация первого прохода, безусловно, может работать как плагин. Таким образом можно разработать логику программы доказательства, не беспокоясь о том, как загружаются двоичные файлы. Как только он окажется работоспособным (понял?), Логику можно будет извлечь и построить для работы с синтаксическими деревьями, созданными другим загрузчиком сборок (с открытым исходным кодом).
Контракты кода не требуют компилятора C #, поскольку они реализованы как классы в .NET Framework 4.0. Можно использовать любой компилятор .NET, который может генерировать управляемую сборку, хотя C ++ / CLI, скорее всего, выдаст несовместимую сборку при смешивании управляемого и собственного кода.
IDE выполняет дополнительные инструменты для перезаписи результирующего IL, чтобы контракты появляются в правильном месте, и поэтому авторам проекта Mono придется написать аналогичные инструменты для контрактов для работы на платформе Mono.
См. этот пост для получения дополнительной информации.