SPARK (язык программирования)
| SPARK | |
|---|---|
 | |
| Класс языка | мультипарадигмальный |
| Появился в | 1988 |
| Разработчик | Altran, AdaCore |
| Выпуск | 22 (2021) |
| Система типов | статическая, строгая, безопасная, номинативная |
| Основные реализации | SPARK Pro, SPARK GPL Edition |
| Испытал влияние | Ада, Eiffel |
| Лицензия | GPLv3 |
| Сайт | adacore.com/about-spark |
| ОС | Linux, Microsoft Windows, macOS |
SPARK (SPADE Ada Kernel[1]) — формально определённый язык программирования, являющийся подмножеством Ады[2], предназначен для разработки верифицированного программного обеспечения высокого уровня полноты безопасности. SPARK позволяет создавать приложения, которые обладают предсказуемым поведением и обеспечивают высокую надёжность.
Версии языка 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].
Концепции[править | править код]
Целью разработки SPARK было сохранение сильных сторон Ады (таких как система пакетов и ограниченные типы) и удаление из неё всех потенциально небезопасных или двусмысленных конструкций[1], так как Ада, несмотря на заявленные цели разработки, получилась довольно сложным языком и не имела полного формального определения[1], а некоторые из её частей вызвали серьёзную критику[12]. Программы SPARK должны быть однозначными, их поведение не должно зависеть от выбора компилятора[К 1], параметров компиляции и состояния окружения. Для этого в язык введены некоторые ограничения, в том числе: использование задач возможно только в профиле Ravenscar; для выражений запрещены побочные эффекты; запрещено использование контролируемых типов, для которых возможно переопределение процедур инициализации и оператора присваивания; запрещено совмещение имён; ограничено использование некоторых операторов, таких как goto; запрещено динамическое выделение памяти (но при этом разрешены типы с динамическими границами и типы с дискриминантами)[2].
При этом любая программа SPARK всё ещё может быть собрана компилятором Ады, что позволяет смешивать эти языки в одном проекте.
Разработчикам SPARK удалось получить удобный для автоматической верификации язык, имеющий простую семантику, строгое формальное определение, логическую корректность и хорошую выразительность[1].
Контракты и зависимости[править | править код]
Для процедуры, которая увеличивает значение некой глобальной переменой на свой аргумент, если тот положительный, и на единицу в прочих случаях, можно написать следующую спецификацию:
procedure Add_to_Total(Value: in Integer)
with
Global => (In_Out => Total),
Depends => (Total => (Total, Value)),
Pre => (Total < Integer'Last - (if Value > 0 then Value else 1)),
Post => (Total = Total'Old + (if Value > 0 then Value else 1));
Аспект Global показывает, к каким глобальным переменным имеет доступ процедура. В данном случае она использует только переменную Total на чтение и запись. Depends показывает взаимосвязь между переменными: новое значение Total зависит от его старого значения и значения Value. Pre — предусловие, оно показывает, какое состояние программы должно быть перед выполнением процедуры; в данном случае в предусловие проверяется, не произойдёт ли переполнение. Post — постусловие, оно показывает состояние программы после выполнения процедуры.
Кроме аспектов подпрограмм предусмотрены и другие способы указывать ограничения на состояние программы, такие как проверочные утверждения:
pragma Assert(Condition);
или инварианты циклов:
pragma Loop_Invariant(Condition);
При этом есть существенные различия в синтаксисе описания контрактов для версий SPARK первого и второго поколений.
Первое поколение языка использовало специальные комментарии:
-- Удвоение натурального числа.
procedure Double(X: in out Natural);
--# pre X < Natural'Last / 2;
--# post X = 2 * X~;
Эквивалентный код для второго поколения:
-- Удвоение натурального числа.
procedure Double(X: in out Natural)
with
Pre => X < Natural'Last / 2,
Post => X = 2 * X'Old;
Верификация[править | править код]
При верификации программ используются следующие приёмы:
- проверка выполнения пред- и постусловий функций;
- проверка отсутствия кода, способного вызвать исключение;
- потоковый анализ зависимостей, который проверяет инициализацию переменных и взаимосвязь между параметрами и результатом работы функций.
Для того, чтобы доказать корректность программы, для всех использованных программистом конструкций, таких как пред- и постусловия, создаются наборы проверочных утверждений. Верификатор GNATprove также может в некоторых случаях самостоятельно генерировать проверочные утверждения. Так, будут выполнены проверки на выход за границы массивов или типов, переполнение и деление на ноль.
Далее, набор проверочных утверждений и данные о начальном состоянии программы, а также полученные от разработчика непроверяемые утверждения, передаются в программу автоматического доказательства. GNATprove при работе использует платформу Why3[13] и системы доказательства проверочных утверждений CVC4, Z3 и Alt-Ergo[14]. Также для доказательства могут быть использованы сторонние системы, такие как Coq[14].
История[править | править код]
Первая версия SPARK (на основе Ada 83) была создана в Саутгемптонском университете при поддержке британского Министерства обороны Бернаром Карре (Bernard Carré) и Тревором Дженнингсом (Trevor Jennings), авторами системы надёжного программирования на Паскале SPADE-Pascal[15]. Далее над усовершенствованием языка работали компании: Program Validation Limited, Praxis Critical Systems Limited (в дальнейшем Altran-Praxis, Altran) и AdaCore.
В начале 2009 года Praxis заключила соглашение с AdaCore и выпустила SPARK Pro на условиях GPL[16]. Затем в июне 2009 была выпущена SPARK GPL Edition, нацеленная на разработку свободного и академического ПО.
О выпуске версии языка второго поколения SPARK 2014 было объявлено 30 апреля 2014 года[17].
См. также[править | править код]
Примечания[править | править код]
Комментарии
- ↑ На 2020 год версию Ada 2012 полноценно поддерживает только один компилятор (GNAT), и SPARK 2014 можно использовать только с ним.
Источники
- ↑ 1 2 3 4 SPARK - The SPADE Ada Kernel (including RavenSPARK). docs.adacore.com. Дата обращения: 10 октября 2020. Архивировано 7 сентября 2021 года.
- ↑ 1 2 Сертификация с помощью SPARK. www.ada-ru.org. Дата обращения: 10 октября 2020. Архивировано 13 мая 2021 года.
- ↑ Johannes Kliemann. Program verification with SPARK - When your code must not fail (2018). Дата обращения: 10 октября 2020. Архивировано 16 мая 2021 года.
- ↑ Eurofighter Typhoon - Customer Projects - AdaCore. www.adacore.com. Дата обращения: 10 октября 2020. Архивировано 21 сентября 2020 года.
- ↑ Самолет Бе-200. www.ada-ru.org. Дата обращения: 10 октября 2020. Архивировано 13 мая 2021 года.
- ↑ GNAT Pro Chosen for UK’s Next Generation ATC System (амер. англ.). AdaCore. Дата обращения: 10 октября 2020. Архивировано 21 сентября 2020 года.
- ↑ Space - AdaCore. www.adacore.com. Дата обращения: 10 октября 2020. Архивировано 21 октября 2020 года.
- ↑ Handy, Alex (2010-08-24). "Ada-derived Skein crypto shows SPARK". SD Times. BZ Media LLC. Архивировано из оригинала 25 августа 2010. Дата обращения: 31 августа 2010.
- ↑ David Hardin, Konrad Slind, Mark Bortz, James Potts, Scott Owens. A High-Assurance, High-Performance Hardware-Based Cross-Domain System (англ.) // Computer Safety, Reliability, and Security / Amund Skavhaug, Jérémie Guiochet, Friedemann Bitsch. — Cham: Springer International Publishing, 2016. — P. 102–113. — ISBN 978-3-319-45477-1. — doi:10.1007/978-3-319-45477-1_9. Архивировано 20 января 2022 года.
- ↑ Genode - Genode Operating System Framework. genode.org. Дата обращения: 10 октября 2020. Архивировано 28 октября 2020 года.
- ↑ Muen | SK for x86/64. muen.sk. Дата обращения: 10 октября 2020. Архивировано 25 октября 2020 года.
- ↑ Henry F. Ledgard, Andrew Singer. Scaling down Ada (or towards a standard Ada subset) // Communications of the ACM. — 1982-02-01. — Т. 25, вып. 2. — С. 121–125. — ISSN 0001-0782. — doi:10.1145/358396.358402.
- ↑ Why3. why3.lri.fr. Дата обращения: 10 октября 2020. Архивировано 12 октября 2020 года.
- ↑ 1 2 Alternative Provers — SPARK User's Guide 22.0w. docs.adacore.com. Дата обращения: 10 октября 2020. Архивировано 12 октября 2020 года.
- ↑ Bernard Carré. Reliable programming in standard languages (англ.) // High-Integrity Software / C. T. Sennett. — Boston, MA: Springer US, 1989. — P. 102–121. — ISBN 978-1-4684-5775-9. — doi:10.1007/978-1-4684-5775-9_5.
- ↑ Praxis and AdaCore Announce SPARK Pro (англ.). AdaCore. Дата обращения: 10 октября 2020. Архивировано 21 сентября 2020 года.
- ↑ Use of SPARK in a Certification Context (англ.). The AdaCore Blog. Дата обращения: 10 октября 2020. Архивировано 12 октября 2020 года.
Литература[править | править код]
- John Barnes. SPARK: The Proven Approach to High Integrity Software. — Altran Praxis, 2012. — ISBN 978-0-9572905-1-8. Архивная копия от 14 октября 2016 на Wayback Machine
- John W. McCormick and Peter C. Chapin. Building High Integrity Applications with SPARK 2014. — Cambridge University Press, 2015. — ISBN 978-1-107-65684-0.
- Барнс Дж., Брасгол Б. Безопасное и надежное программное обеспечение на примере языка Ада 2012, SPARK 2014. — 2015. — 154 с.
- Yannick Moy. SPARK Ada for the MISRA C Developer. — 2019.