Dafny — язык программирования
Dafny — это язык программирования, вдохновлённый такими языками, как Euclid, Eiffel, CLU, Java, C
Основные функции
Среди основных функций Dafny можно выделить:- обобщённые классы;
- индуктивные типы данных;
- динамическое выделение памяти;
- неявные динамические фреймы (производные от логики разделения).
Язык в основном используется для обучения формальной спецификации и верификации. Также он часто применяется на соревнованиях для проверки программного обеспечения.
Поскольку Dafny основан на промежуточном языке Boogie, он использует Z3, который включён в загруженный пакет. После распаковки архива вы можете запустить «dafny /help», чтобы просмотреть список поддерживаемых команд.
Команды
Например, вы можете выбрать файл прелюдии Dafny (/dprelude:Также доступны параметры Boogie, такие как разрешение только синтаксического анализа (/noResolve) или только синтаксического анализа и разрешения (/noTypeCheck). Дополнительные команды могут использоваться для логического вывода, отладки и общего отслеживания, генерации условий проверки и разделения CIVL и т. д.
Плюсы программы:- Обучение формальной спецификации и верификации.
- Применение на соревнованиях по проверке ПО.
- Поддержка предусловий и постусловий.
- Использование промежуточного языка Boogie и Z3.
- Наличие множества команд для различных целей.
Похожие программы
| Категория | Языки программирования/компиляторы |
| Версия | 4.4.0 |
| Разработчик | Rustan Leino |
| Размер | 60 MB |
| Лицензия | MIT License |
| ОС |
|