|
SPARK (язык программирования)
SPARK (SPADE Ada Kernel[1]) — формально определённый язык программирования, являющийся подмножеством Ады[2], предназначен для разработки верифицированного программного обеспечения высокого уровня полноты безопасности[англ.]. 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[3], самолёты Eurofighter Typhoon[4] и Бе-200[5], система UK NATS iFACTS[6]) и для разработки космических систем (РН Вега, множество спутников[7]). Также его применяют для разработки систем шифрования[8] и кибербезопасности[9][10][11]. КонцепцииЦелью разработки 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]. См. такжеПримечанияКомментарии
Источники
Литература
СсылкиInformation related to SPARK (язык программирования) |
||||||||||||||||||||||||
