SPARK (мова програмування)
SPARK (SPADE Ada Kernel[3]) — формально визначена мова програмування, що є підмножиною Ади[4], призначена для розробки верифікованого програмного забезпечення високого рівня повноти безпечності. 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[5], літаки Eurofighter Typhoon[6] та Бе-200[7], система UK NATS iFACTS[8]) та для розробки космічних систем (РН Вега, багато супутників[9])). Також її застосовують для розробки систем шифрування[10] та кібербезпеки[11][12][13].
Метою розробки SPARK було збереження сильних сторін Ади (таких як система пакунків та обмежені типи) та видалення з неї всіх потенційно небезпечних або двозначних конструкцій[3], оскільки Ада, попри заявлені цілі розробки, вийшла досить складною мовою і не мала повного формального визначення[3], а деякі її частини викликали серйозну критику[14]. Програми SPARK мають бути однозначними, їхня поведінка не повинна залежати від вибору компілятора[К 1], параметрів компіляції та стану оточення. Для цього в мову введено деякі обмеження, зокрема: використання задач можливе лише у профілі Ravenscar; для виразів заборонено побічні ефекти; заборонено використання контрольованих типів, для яких можливе перевизначення процедур ініціалізації та оператора присвоєння; заборонено суміщення назв; обмежено використання деяких операторів, таких як goto; заборонено динамічне виділення пам'яті (але при цьому дозволено типи з динамічними межами та типи з дискримінантами)[4].
При цьому будь-яку програму SPARK все ще можна зібрати компілятором Ади, що дозволяє змішувати ці мови в одному проєкті.
Розробникам SPARK вдалося отримати зручну для автоматичної верифікації мову, що має просту семантику, строге формальне визначення, логічну коректність і виразність[3].
Для процедури, яка збільшує значення деякої глобальної зміної на свій аргумент, якщо той додатний, і на одиницю в інших випадках, можна написати таку специфікацію:
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[15] та системи доведення перевіряльних тверджень CVC4, Z3 та Alt-Ergo[16]. Також для доведення можна використати сторонні системи, такі як Coq[16].
Першу версію SPARK (на основі Ada 83) створили в Саутгемптонському університеті за підтримки британського Міністерства оборони Бернар Карре (Bernard Carré) і Тревор Дженнінгс (Trevor Jennings), автори системи надійного програмування на Паскалі SPADE-Pascal[17]. Далі над удосконаленням мови працювали компанії: Program Validation Limited, Praxis Critical Systems Limited (надалі Altran-Praxis, Altran) та AdaCore.
На початку 2009 Praxis уклала угоду з AdaCore і випустила SPARK Pro на умовах GPL[18]. Потім у червні 2009 року випущено SPARK GPL Edition, націлену на розробку вільного та академічного ПЗ.
Про випуск версії мови другого покоління SPARK 2014 оголошено 30 квітня 2014 року[19].
- Коментарі
- ↑ На 2020 рік версію Ada 2012 повноцінно підтримує лише один компілятор (GNAT), і SPARK 2014 можна використовувати тільки з ним.
- Джерела
- ↑ (unspecified title) — doi:10.1007/978-1-4684-5775-9_5
- ↑ https://github.com/AdaCore/spark2014/blob/master/LICENSE
- ↑ а б в г SPARK - The SPADE Ada Kernel (including RavenSPARK). docs.adacore.com. Архів оригіналу за 7 вересня 2021. Процитовано 10 жовтня 2020.
- ↑ а б Сертификация с помощью SPARK. www.ada-ru.org. Архів оригіналу за 13 травня 2021. Процитовано 10 жовтня 2020.
- ↑ Johannes Kliemann (2018). Program verification with SPARK - When your code must not fail. Архів оригіналу за 16 травня 2021. Процитовано 10 жовтня 2020.
- ↑ Eurofighter Typhoon - Customer Projects - AdaCore. www.adacore.com. Архів оригіналу за 21 вересня 2020. Процитовано 10 жовтня 2020.
- ↑ Самолет Бе-200. www.ada-ru.org. Архів оригіналу за 13 травня 2021. Процитовано 10 жовтня 2020.
- ↑ GNAT Pro Chosen for UK’s Next Generation ATC System. AdaCore (амер.). Архів оригіналу за 21 вересня 2020. Процитовано 10 жовтня 2020.
- ↑ Space - AdaCore. www.adacore.com. Архів оригіналу за 21 жовтня 2020. Процитовано 10 жовтня 2020.
- ↑ Handy, Alex (24 серпня 2010). Ada-derived Skein crypto shows SPARK. SD Times. BZ Media LLC. Архів оригіналу за 25 серпня 2010. Процитовано 31 серпня 2010.
- ↑ David Hardin, Konrad Slind, Mark Bortz, James Potts, Scott Owens. A High-Assurance, High-Performance Hardware-Based Cross-Domain System / Amund Skavhaug, Jérémie Guiochet, Friedemann Bitsch // Computer Safety, Reliability, and Security. — Cham : Springer International Publishing, 2016. — 9 November. — P. 102–113. — ISBN 978-3-319-45477-1. — DOI:. Архівовано з джерела 20 січня 2022.
- ↑ Genode - Genode Operating System Framework. genode.org. Архів оригіналу за 28 жовтня 2020. Процитовано 10 жовтня 2020.
- ↑ Muen | SK for x86/64. muen.sk. Архів оригіналу за 25 жовтня 2020. Процитовано 10 жовтня 2020.
- ↑ Henry F. Ledgard, Andrew Singer. Scaling down Ada (or towards a standard Ada subset) // Communications of the ACM. — 1982. — Т. 25, вип. 2 (1 лютого). — С. 121–125. — ISSN 0001-0782. — DOI:.
- ↑ Why3. why3.lri.fr. Архів оригіналу за 12 жовтня 2020. Процитовано 10 жовтня 2020.
- ↑ а б Alternative Provers — SPARK User's Guide 22.0w. docs.adacore.com. Архів оригіналу за 12 жовтня 2020. Процитовано 10 жовтня 2020.
- ↑ Bernard Carré. Reliable programming in standard languages / C. T. Sennett // High-Integrity Software. — Boston, MA : Springer US, 1989. — 9 November. — P. 102–121. — ISBN 978-1-4684-5775-9. — DOI:.
- ↑ Praxis and AdaCore Announce SPARK Pro. AdaCore (англ.). Архів оригіналу за 21 вересня 2020. Процитовано 10 жовтня 2020.
- ↑ Use of SPARK in a Certification Context. The AdaCore Blog (англ.). Архів оригіналу за 12 жовтня 2020. Процитовано 10 жовтня 2020.
- John Barnes (2012). SPARK: The Proven Approach to High Integrity Software. Altran Praxis. ISBN 978-0-9572905-1-8. Архівовано жовтень 14, 2016 на сайті Wayback Machine.
- John W. McCormick and Peter C. Chapin (2015). Building High Integrity Applications with SPARK 2014. Cambridge University Press. ISBN 978-1-107-65684-0.
- Барнс Дж., Брасгол Б. Безопасное и надежное программное обеспечение на примере языка Ада 2012, SPARK 2014. — 2015. — 154 с.
- Yannick Moy. SPARK Ada for the MISRA C Developer. — 2019.
