SPARK ( SPADE Ada Kernel ) — формально определённый язык программирования , являющийся подмножеством Ады , предназначен для разработки верифицированного программного обеспечения высокого . 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 , самолёты Eurofighter Typhoon и Бе-200 , система UK NATS iFACTS ) и для разработки космических систем ( РН Вега , множество спутников ). Также его применяют для разработки систем шифрования и кибербезопасности .

Концепции

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

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

Разработчикам SPARK удалось получить удобный для автоматической верификации язык, имеющий простую семантику, строгое формальное определение, логическую корректность и хорошую выразительность .

Контракты и зависимости

Для процедуры, которая увеличивает значение некой глобальной переменой на свой аргумент, если тот положительный, и на единицу в прочих случаях, можно написать следующую спецификацию:

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

История

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

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

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

См. также

• MISRA C
• Z-нотация
• Статический анализ кода

Примечания

Комментарии

Источники

Литература

• John Barnes. . — Altran Praxis, 2012. — ISBN 978-0-9572905-1-8 . от 14 октября 2016 на Wayback Machine
• John W. McCormick and Peter C. Chapin. . — Cambridge University Press, 2015. — ISBN 978-1-107-65684-0 .
• Барнс Дж., Брасгол Б. . — 2015. — 154 с.
• Yannick Moy. . — 2019.

Ссылки

• от 12 февраля 2005 на Wayback Machine