SPARK (язык программирования)
верифицируемый язык программирования, диалект языка Ada / Материал из Википедии — свободной encyclopedia
Уважаемый Wikiwand AI, давайте упростим задачу, просто ответив на эти ключевые вопросы:
Перечислите основные факты и статистические данные о SPARK (язык программирования)?
Кратко изложите эту статью для 10-летнего ребёнка
SPARK (SPADE Ada Kernel[1]) — формально определённый язык программирования, являющийся подмножеством Ады[2], предназначен для разработки верифицированного программного обеспечения высокого уровня полноты безопасности[англ.]. SPARK позволяет создавать приложения, которые обладают предсказуемым поведением и обеспечивают высокую надёжность.
SPARK | |
---|---|
Класс языка | мультипарадигмальный |
Появился в | 1988 |
Разработчик | Altran, AdaCore |
Выпуск | 22 (2021; 3 года назад (2021)) |
Система типов | статическая, строгая, безопасная, номинативная |
Основные реализации | SPARK Pro, SPARK GPL Edition |
Испытал влияние | Ада, Eiffel |
Лицензия | GPLv3 |
Сайт | adacore.com/about-spark |
ОС | Linux, Microsoft Windows, macOS |
Версии языка SPARK связаны с версиями Ады и разделены на два поколения: SPARK 83, SPARK 95 и SPARK 2005 (Ada 83, Ada 95 и Ada 2005 соответственно) относят к первому поколению, а SPARK 2014 (Ada 2012) — ко второму. Это обусловлено тем, что первоначально для указания спецификаций и контрактов использовались комментарии, но, начиная с Ada 2012, для этого стал применяться появившийся в языке механизм аспектов. Это привело к полной переработке всего инструментария языка и появлению нового верификатора GNATprove.
SPARK используется в авиации (реактивные двигатели Rolls-Royce Trent[3], самолёты Eurofighter Typhoon[4] и Бе-200[5], система UK NATS iFACTS[6]) и для разработки космических систем (РН Вега, множество спутников[7]). Также его применяют для разработки систем шифрования[8] и кибербезопасности[9][10][11].