SPARK (язык программирования)

SPARK (SPADE Ada Kernel[1]) — это формально определенный язык программирования, представляющий собой подмножество языка Ada[2], предназначенный для разработки верифицированного программного обеспечения высокого уровня полноты безопасности[en]. SPARK позволяет создавать приложения, которые обладают предсказуемым поведением и обеспечивают высокую надёжность.

SPARK
Изображение логотипа
Класс языка мультипарадигмальный
Появился в 1988
Разработчик Altran, AdaCore
Выпуск 22 (2021; 1 год назад (2021))
Система типов статическая, строгая, безопасная, номинативная
Основные реализации SPARK Pro, SPARK GPL Edition
Испытал влияние Ада, Eiffel
Лицензия GPLv3
Сайт adaic.org/advantages/spa…
ОС Linux, Microsoft Windows, Mac OS X

Версии языка SPARK связаны с версиями Ada и разделены на два поколения: SPARK 83, SPARK 95 и SPARK 2005 (Ada 83, Ada 95 и Ada 2005 соответственно) относят к первому поколению, а SPARK 2014 (Ada 2012) — ко второму.

Это обусловлено тем, что первоначально для указания спецификаций и контрактов использовались комментарии, но, начиная с Ada 2012, для этого стал применяться появившийся в языке механизм аспектов. Это привело к полной переработке всего инструментария языка и появлению нового верификатора GNATprove.

Описание языкаПравить

Целью разработки SPARK было сохранение сильных сторон языка Ada (таких как система пакетов и ограниченные типы) и удаление из него всех потенциально небезопасных или двусмысленных конструкций[1], так как язык Ada, несмотря на заявленные цели разработки, получился довольно сложным и не имел полного формального определения[1], а некоторые из его частей вызвали серьёзную критику[3]. Программы SPARK должны быть однозначными, их поведение не должно зависеть от выбора компилятора[К 1], параметров компиляции и состояния окружения. Для этого в язык введены некоторые ограничения, в том числе: использование задач возможно только в профиле Ravenscar; для выражений запрещены побочные эффекты; запрещено использование контроллируемых типов, для которых возможно переопределение процедур инициализации и оператора присваивания; запрещено совмещение имён; ограничено использование некоторых операторов, таких как goto; запрещено динамическое выделение памяти (но при этом разрешены типы с динамическими границами и типы с дискриминантами)[2].

При этом любая программа SPARK всё ещё может быть собрана компилятором Ada, что позволяет смешивать эти языки в одном проекте.

Разработчикам 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[4] и системы доказательства проверочных утверждений CVC4, Z3 и Alt-Ergo[5]. Также для доказательства могут быть использованы сторонние системы, такие как Coq[5].

ИсторияПравить

Первая версия SPARK (на основе Ada 83) была создана в Саутгемптонском университете при поддержке британского Министерства обороны Бернаром Карре (Bernard Carré) и Тревором Дженнингсом (Trevor Jennings), авторами системы надёжного программирования на Паскале SPADE-Pascal[6]. Далее над усовершенствованием языка работали компании: Program Validation Limited, Praxis Critical Systems Limited (в дальнейшем Altran-Praxis, Altran) и AdaCore.

В начале 2009 года Praxis заключила соглашение с AdaCore и выпустила SPARK Pro на условиях GPL[7]. Затем в июне 2009 была выпущена SPARK GPL Edition, нацеленная на разработку свободного и академического ПО.

О выпуске версии языка второго поколения SPARK 2014 было объявлено 30 апреля 2014 года[8].

Промышленное применениеПравить

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

ЛитератураПравить

СсылкиПравить