Оглавление [Скрыть]
SPARK (язык программирования)
-
Определение и история SPARK
- SPARK – это язык программирования, основанный на Ada, предназначенный для разработки высоконадежного ПО.
- Язык имеет четыре версии, начиная с SPARK83 и заканчивая SPARK 2014.
- SPARK 2014 является полной переработкой с улучшенной проверкой и поддержкой контрактов.
-
Особенности и применение SPARK
- SPARK стремится к логической обоснованности, строгой формализации и простоте семантики.
- Язык обеспечивает безопасность, выразительность, проверяемость и минимальные системные требования.
- Примеры контрактов в SPARK 2014 показывают, как спецификации подпрограмм могут быть уточнены для обеспечения ясности и предсказуемости.
-
Инструменты и проверка
- GNATprove, основанный на GNAT/GCC, использует контракты для проверки соответствия спецификации и кода.
- SPARK 2014 генерирует условия проверки (VCS) для обеспечения отсутствия ошибок во время выполнения.
-
История и развитие
- SPARK был разработан в Университете Саутгемптона и получил свое название от SPADE Ada Kernel.
- Язык был усовершенствован различными компаниями, включая Praxis Critical Systems Limited и Altran Praxis.
- SPARK использовался в различных критически важных системах, включая авиацию, управление воздушным движением и космонавтику.
-
Производительность и безопасность
- SPARK продемонстрировал высокую производительность, сравнимую с C, и был использован для реализации критически важных функций безопасности, таких как SHA-3 и TweetNaCl.
-
Дополнительные ресурсы
- Ссылки на веб-сайты сообщества SPARK 2014 и другие ресурсы, связанные с языком, предоставлены в статье.