SPARK (язык программирования): различия между версиями

Материал из Википедии — свободной энциклопедии
Перейти к навигации Перейти к поиску
Следующая правка →
Содержимое удалено Содержимое добавлено
ВизуальныйВики-текст
Создано переводом страницы «SPARK (programming language)»
(нет различий)

Версия от 17:32, 10 октября 2020

У этого термина существуют и другие значения, см. Spark.
SPARK
Класс языка мультипарадигмальный
Появился в 1988
Разработчик Altran, AdaCore
Выпуск 20.0 (26 мая 2020; 4 года назад (2020-05-26))
Система типов статическая, строгая, безопасная, номинативная
Основные реализации SPARK Pro, SPARK GPL Edition
Испытал влияние Ада, Eiffel
Лицензия GPLv3
Сайт adaic.org/advantages/spa…
ОС Linux, Microsoft Windows, Mac OS X

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

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

Литература

Ссылки

Источник — https://ru.wikipedia.org/w/index.php?title=SPARK_(язык_программирования)&oldid=109799566