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 должны быть однозначными, их поведение не должно зависеть от выбора компилятораНа 2020 год версию Ada 2012 полноценно поддерживает только один компилятор (GNAT), и SPARK 2014 можно использовать только с ним., параметров компиляции и состояния окружения. Для этого в язык введены некоторые ограничения, в том числе: использование задач возможно только в профиле 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-нотация Статический анализ кода

Примечания Комментарии

Источники

Литература

Ссылки Страница SPARK Ada на сайте Ada Resource Association SPARK Pro SPARK Libre Справка по SPARK 2014

Категория:Языки программирования, появившиеся в XX веке Категория:Процедурные языки программирования Категория:Языки формальных спецификаций Категория:Языки программирования семейства Алгола Категория:Ада