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 (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].

См. также

Примечания

Комментарии

  1. ↑ На 2020 год версию Ada 2012 полноценно поддерживает только один компилятор (GNAT), и SPARK 2014 можно использовать только с ним.

Источники

  1. ↑ 1 2 3 4 SPARK - The SPADE Ada Kernel (including RavenSPARK). docs.adacore.com. Дата обращения: 10 октября 2020. Архивировано 7 сентября 2021 года.
  2. ↑ 1 2 Сертификация с помощью SPARK. www.ada-ru.org. Дата обращения: 10 октября 2020. Архивировано 13 мая 2021 года.
  3. ↑ Johannes Kliemann. Program verification with SPARK - When your code must not fail (2018). Дата обращения: 10 октября 2020. Архивировано 16 мая 2021 года.
  4. ↑ Eurofighter Typhoon - Customer Projects - AdaCore. www.adacore.com. Дата обращения: 10 октября 2020. Архивировано 21 сентября 2020 года.
  5. ↑ Самолет Бе-200. www.ada-ru.org. Дата обращения: 10 октября 2020. Архивировано 13 мая 2021 года.
  6. ↑ GNAT Pro Chosen for UK’s Next Generation ATC System (амер. англ.). AdaCore. Дата обращения: 10 октября 2020. Архивировано 21 сентября 2020 года.
  7. ↑ Space - AdaCore. www.adacore.com. Дата обращения: 10 октября 2020. Архивировано 21 октября 2020 года.
  8. ↑ Handy, Alex (2010-08-24). "Ada-derived Skein crypto shows SPARK". SD Times. BZ Media LLC. Архивировано 25 августа 2010. Дата обращения: 31 августа 2010.
  9. ↑ 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 года.
  10. ↑ Genode - Genode Operating System Framework. genode.org. Дата обращения: 10 октября 2020. Архивировано 28 октября 2020 года.
  11. ↑ Muen | SK for x86/64. muen.sk. Дата обращения: 10 октября 2020. Архивировано 25 октября 2020 года.
  12. ↑ 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.
  13. ↑ Why3. why3.lri.fr. Дата обращения: 10 октября 2020. Архивировано 12 октября 2020 года.
  14. ↑ 1 2 Alternative Provers — SPARK User's Guide 22.0w. docs.adacore.com. Дата обращения: 10 октября 2020. Архивировано 12 октября 2020 года.
  15. ↑ 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.
  16. ↑ Praxis and AdaCore Announce SPARK Pro (англ.). AdaCore. Дата обращения: 10 октября 2020. Архивировано 21 сентября 2020 года.
  17. ↑ Use of SPARK in a Certification Context (англ.). The AdaCore Blog. Дата обращения: 10 октября 2020. Архивировано 12 октября 2020 года.

Литература

Ссылки