Описание тега dafny

Dafny - это язык программирования со встроенными конструкциями спецификаций. Верификатор статических программ Dafny может использоваться для проверки функциональной корректности программ.

Язык программирования Dafny разработан для поддержки статической проверки программ. Он является императивным, последовательным, поддерживает общие классы, динамическое размещение и индуктивные типы данных, а также встраивает конструкции спецификаций. Спецификации включают предварительные и постусловия, спецификации кадра (наборы для чтения и записи) и метрики завершения. Для дальнейшей поддержки спецификаций язык также предлагает обновляемые призрачные переменные, рекурсивные функции и типы, такие как наборы и последовательности. Спецификации и призрачные конструкции используются только при проверке; компилятор исключает их из исполняемого кода.

Верификатор Dafny запускается как часть компилятора. Таким образом, программист взаимодействует с ним почти так же, как со средством проверки статического типа - когда инструмент выдает ошибки, программист реагирует, изменяя объявления типов, спецификации и операторы программы.

Домашняя страница: http://research.microsoft.com/en-us/projects/dafny/