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

Целью разработки 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].