Azərbaycanca AzərbaycancaБеларускі БеларускіDansk DanskDeutsch DeutschEspañola EspañolaFrançais FrançaisIndonesia IndonesiaItaliana Italiana日本語 日本語Қазақ ҚазақLietuvos LietuvosNederlands NederlandsPortuguês PortuguêsРусский Русскийසිංහල සිංහලแบบไทย แบบไทยTürkçe TürkçeУкраїнська Українська中國人 中國人United State United StateAfrikaans Afrikaans
Підтримка
www.wikidata.uk-ua.nina.az

SPARK SPADE Ada Kernel формально визначена мова програмування що є підмножиною Ади призначена для розробки верифікованог

SPARK (мова програмування)

SPARK (мова програмування)

SPARK (SPADE Ada Kernel) — формально визначена мова програмування, що є підмножиною Ади, призначена для розробки верифікованого програмного забезпечення високого рівня повноти безпечності. SPARK дозволяє створювати програми, які мають передбачувану поведінку і забезпечують високу надійність.

SPARK
Парадигмапроцедурне програмування
Дата появи1988
Розробникd і Університет Саутгемптона
Система типізаціїd, статична, строга типізація і типобезпечність
Мова реалізаціїАда
ЛіцензіяGNU GPL 3[2]
Репозиторій вихідного кодуgithub.com/AdaCore/spark2014
Вебсайтadacore.com/sparkpro/

Версії мови SPARK пов'язані з версіями Ади й поділені на два покоління: SPARK 83, SPARK 95 і SPARK 2005 (Ada 83, Ada 95 та Ada 2005 відповідно) відносять до першого покоління, а SPARK 2014 (Ada 2012) — до другого. Це зумовлено тим, що спочатку для вказання специфікацій і контрактів використовувалися коментарі, але, починаючи з Ada 2012, для цього стали застосовувати механізм аспектів, що з'явився в мові. Це призвело до повної переробки всього інструментарію мови та появи нового верифікатора GNATprove.

SPARK використовують у авіації (реактивні двигуни [en], літаки 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 року.

Див. також

Примітки

Коментарі
  1. На 2020 рік версію Ada 2012 повноцінно підтримує лише один компілятор (GNAT), і SPARK 2014 можна використовувати тільки з ним.
Джерела
  1. (unspecified title) — doi:10.1007/978-1-4684-5775-9_5
  2. https://github.com/AdaCore/spark2014/blob/master/LICENSE
  3. SPARK - The SPADE Ada Kernel (including RavenSPARK). docs.adacore.com. оригіналу за 7 вересня 2021. Процитовано 10 жовтня 2020.
  4. Сертификация с помощью SPARK. www.ada-ru.org. оригіналу за 13 травня 2021. Процитовано 10 жовтня 2020.
  5. Johannes Kliemann (2018). Program verification with SPARK - When your code must not fail. оригіналу за 16 травня 2021. Процитовано 10 жовтня 2020.
  6. Eurofighter Typhoon - Customer Projects - AdaCore. www.adacore.com. оригіналу за 21 вересня 2020. Процитовано 10 жовтня 2020.
  7. Самолет Бе-200. www.ada-ru.org. оригіналу за 13 травня 2021. Процитовано 10 жовтня 2020.
  8. GNAT Pro Chosen for UK’s Next Generation ATC System. AdaCore (en-US) . оригіналу за 21 вересня 2020. Процитовано 10 жовтня 2020.
  9. Space - AdaCore. www.adacore.com. оригіналу за 21 жовтня 2020. Процитовано 10 жовтня 2020.
  10. Handy, Alex (24 серпня 2010). . . BZ Media LLC. Архів оригіналу за 25 серпня 2010. Процитовано 31 серпня 2010.
  11. 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. — 5 July. — P. 102–113. — . — DOI:10.1007/978-3-319-45477-1_9. з джерела 20 січня 2022.
  12. Genode - Genode Operating System Framework. genode.org. оригіналу за 28 жовтня 2020. Процитовано 10 жовтня 2020.
  13. Muen | SK for x86/64. muen.sk. оригіналу за 25 жовтня 2020. Процитовано 10 жовтня 2020.
  14. 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:10.1145/358396.358402.
  15. Why3. why3.lri.fr. оригіналу за 12 жовтня 2020. Процитовано 10 жовтня 2020.
  16. Alternative Provers — SPARK User's Guide 22.0w. docs.adacore.com. оригіналу за 12 жовтня 2020. Процитовано 10 жовтня 2020.
  17. Bernard Carré. Reliable programming in standard languages / C. T. Sennett // High-Integrity Software. — Boston, MA : Springer US, 1989. — 5 July. — P. 102–121. — . — DOI:10.1007/978-1-4684-5775-9_5.
  18. Praxis and AdaCore Announce SPARK Pro. AdaCore (англ.). оригіналу за 21 вересня 2020. Процитовано 10 жовтня 2020.
  19. 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 . Архівовано жовтень 14, 2016 на сайті Wayback Machine.
  • John W. McCormick and Peter C. Chapin (2015). Building High Integrity Applications with SPARK 2014. Cambridge University Press. ISBN .
  • Барнс Дж., Брасгол Б. Безопасное и надежное программное обеспечение на примере языка Ада 2012, SPARK 2014. — 2015. — 154 с.
  • Yannick Moy. SPARK Ada for the MISRA C Developer. — 2019.

Посилання

  • Сторінка SPARK Ada на сайті Ada Resource Association
  • SPARK Pro
  • SPARK Libre Архівна копія на сайті Wayback Machine.
  • Довідка зі SPARK 2014

Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет

SPARK SPADE Ada Kernel formalno viznachena mova programuvannya sho ye pidmnozhinoyu Adi priznachena dlya rozrobki verifikovanogo programnogo zabezpechennya visokogo rivnya povnoti bezpechnosti SPARK dozvolyaye stvoryuvati programi yaki mayut peredbachuvanu povedinku i zabezpechuyut visoku nadijnist SPARKParadigmaprocedurne programuvannyaData poyavi1988Rozrobnikd i Universitet SautgemptonaSistema tipizaciyid statichna stroga tipizaciya i tipobezpechnistMova realizaciyiAdaLicenziyaGNU GPL 3 2 Repozitorij vihidnogo kodugithub com AdaCore spark2014Vebsajtadacore com sparkpro Versiyi movi SPARK pov yazani z versiyami Adi j podileni na dva pokolinnya SPARK 83 SPARK 95 i SPARK 2005 Ada 83 Ada 95 ta Ada 2005 vidpovidno vidnosyat do pershogo pokolinnya a SPARK 2014 Ada 2012 do drugogo Ce zumovleno tim sho spochatku dlya vkazannya specifikacij i kontraktiv vikoristovuvalisya komentari ale pochinayuchi z Ada 2012 dlya cogo stali zastosovuvati mehanizm aspektiv sho z yavivsya v movi Ce prizvelo do povnoyi pererobki vsogo instrumentariyu movi ta poyavi novogo verifikatora GNATprove SPARK vikoristovuyut u aviaciyi reaktivni dviguni en litaki Eurofighter Typhoon ta Be 200 sistema UK NATS iFACTS ta dlya rozrobki kosmichnih sistem RN Vega bagato suputnikiv Takozh yiyi zastosovuyut dlya rozrobki sistem shifruvannya ta kiberbezpeki KoncepciyaMetoyu rozrobki SPARK bulo zberezhennya silnih storin Adi takih yak sistema pakunkiv ta obmezheni tipi ta vidalennya z neyi vsih potencijno nebezpechnih abo dvoznachnih konstrukcij oskilki Ada popri zayavleni cili rozrobki vijshla dosit skladnoyu movoyu i ne mala povnogo formalnogo viznachennya a deyaki yiyi chastini viklikali serjoznu kritiku Programi SPARK mayut buti odnoznachnimi yihnya povedinka ne povinna zalezhati vid viboru kompilyatora parametriv kompilyaciyi ta stanu otochennya Dlya cogo v movu vvedeno deyaki obmezhennya zokrema vikoristannya mozhlive lishe u profili Ravenscar dlya viraziv zaboroneno pobichni efekti zaboroneno vikoristannya kontrolovanih tipiv dlya yakih mozhlive pereviznachennya procedur inicializaciyi ta operatora prisvoyennya zaboroneno sumishennya nazv obmezheno vikoristannya deyakih operatoriv takih yak goto zaboroneno dinamichne vidilennya pam yati ale pri comu dozvoleno tipi z dinamichnimi mezhami ta tipi z diskriminantami Pri comu bud yaku programu SPARK vse she mozhna zibrati kompilyatorom Adi sho dozvolyaye zmishuvati ci movi v odnomu proyekti Rozrobnikam SPARK vdalosya otrimati zruchnu dlya avtomatichnoyi verifikaciyi movu sho maye prostu semantiku stroge formalne viznachennya logichnu korektnist i viraznist Kontrakti j zalezhnostiDlya proceduri yaka zbilshuye znachennya deyakoyi globalnoyi zminoyi na svij argument yaksho toj dodatnij i na odinicyu v inshih vipadkah mozhna napisati taku specifikaciyu procedure Add to Total Value in Integer with Global gt In Out gt Total Depends gt Total gt Total Value Pre gt Total lt Integer Last if Value gt 0 then Value else 1 Post gt Total Total Old if Value gt 0 then Value else 1 Aspekt Global pokazuye do yakih globalnih zminnih maye dostup procedura V comu vipadku vona vikoristovuye lishe zminnu Total na chitannya ta zapis Depends pokazuye vzayemozv yazok mizh zminnimi nove znachennya Total zalezhit vid jogo starogo znachennya i znachennya Value Pre peredumova vono pokazuye yakim maye buti stan programi pered vikonannyam proceduri u comu razi v peredumovi pereviryayetsya chi ne trapitsya perepovnennya Post pislyaumova vona pokazuye stan programi pislya vikonannya proceduri Krim aspektiv pidprogram peredbacheno inshi sposobi vkazuvati obmezhennya na stan programi taki yak perevirkovi tverdzhennya pragma Assert Condition abo invarianti cikliv pragma Loop Invariant Condition Pri comu ye suttyevi vidminnosti v sintaksisi opisu kontraktiv dlya versij SPARK pershogo ta drugogo pokolin Pershe pokolinnya movi vikoristovuvalo specialni komentari Podvoyennya naturalnogo chisla procedure Double X in out Natural pre X lt Natural Last 2 post X 2 X Ekvivalentnij kod dlya drugogo pokolinnya Podvoyennya naturalnogo chisla procedure Double X in out Natural with Pre gt X lt Natural Last 2 Post gt X 2 X Old VerifikaciyaPid chas verifikaciyi program vikoristovuyut taki prijomi perevirka vikonannya pered ta pislyaumov funkcij perevirka vidsutnosti kodu zdatnogo sprichiniti vinyatok potokovij analiz zalezhnostej yakij pereviryaye inicializaciyu zminnih ta vzayemozv yazok mizh parametrami ta rezultatom roboti funkcij Dlya togo shob dovesti korektnist programi dlya vsih vikoristanih programistom konstrukcij takih yak pered ta pislyaumovi stvoryuyutsya nabori pereviryalnih tverdzhen Verifikator GNATprove takozh mozhe v deyakih vipadkah samostijno generuvati pereviryalni tverdzhennya Tak bude vikonano perevirki na vihid za mezhi masiviv abo tipiv perepovnennya ta dilennya na nul Dali nabir pereviryalnih tverdzhen ta dani pro pochatkovij stan programi a takozh otrimani vid rozrobnika neperevireni tverdzhennya peredayutsya v programu avtomatichnogo dovedennya GNATprove pid chas roboti vikoristovuye platformu Why3 ta sistemi dovedennya pereviryalnih tverdzhen CVC4 Z3 ta Alt Ergo Takozh dlya dovedennya mozhna vikoristati storonni sistemi taki yak Coq IstoriyaPershu versiyu SPARK na osnovi Ada 83 stvorili v Sautgemptonskomu universiteti za pidtrimki britanskogo Ministerstva oboroni Bernar Karre Bernard Carre i Trevor Dzhennings Trevor Jennings avtori sistemi nadijnogo programuvannya na Paskali SPADE Pascal Dali nad udoskonalennyam movi pracyuvali kompaniyi Program Validation Limited Praxis Critical Systems Limited nadali Altran Praxis Altran ta AdaCore Na pochatku 2009 Praxis uklala ugodu z AdaCore i vipustila SPARK Pro na umovah GPL Potim u chervni 2009 roku vipusheno SPARK GPL Edition nacilenu na rozrobku vilnogo ta akademichnogo PZ Pro vipusk versiyi movi drugogo pokolinnya SPARK 2014 ogolosheno 30 kvitnya 2014 roku Div takozh en Z notaciya Statichnij analiz koduPrimitkiKomentari Na 2020 rik versiyu Ada 2012 povnocinno pidtrimuye lishe odin kompilyator GNAT i SPARK 2014 mozhna vikoristovuvati tilki z nim Dzherela 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 originalu za 7 veresnya 2021 Procitovano 10 zhovtnya 2020 Sertifikaciya s pomoshyu SPARK www ada ru org originalu za 13 travnya 2021 Procitovano 10 zhovtnya 2020 Johannes Kliemann 2018 Program verification with SPARK When your code must not fail originalu za 16 travnya 2021 Procitovano 10 zhovtnya 2020 Eurofighter Typhoon Customer Projects AdaCore www adacore com originalu za 21 veresnya 2020 Procitovano 10 zhovtnya 2020 Samolet Be 200 www ada ru org originalu za 13 travnya 2021 Procitovano 10 zhovtnya 2020 GNAT Pro Chosen for UK s Next Generation ATC System AdaCore en US originalu za 21 veresnya 2020 Procitovano 10 zhovtnya 2020 Space AdaCore www adacore com originalu za 21 zhovtnya 2020 Procitovano 10 zhovtnya 2020 Handy Alex 24 serpnya 2010 BZ Media LLC Arhiv originalu za 25 serpnya 2010 Procitovano 31 serpnya 2010 David Hardin Konrad Slind Mark Bortz James Potts Scott Owens A High Assurance High Performance Hardware Based Cross Domain System Amund Skavhaug Jeremie Guiochet Friedemann Bitsch Computer Safety Reliability and Security Cham Springer International Publishing 2016 5 July P 102 113 ISBN 978 3 319 45477 1 DOI 10 1007 978 3 319 45477 1 9 z dzherela 20 sichnya 2022 Genode Genode Operating System Framework genode org originalu za 28 zhovtnya 2020 Procitovano 10 zhovtnya 2020 Muen SK for x86 64 muen sk originalu za 25 zhovtnya 2020 Procitovano 10 zhovtnya 2020 Henry F Ledgard Andrew Singer Scaling down Ada or towards a standard Ada subset Communications of the ACM 1982 T 25 vip 2 1 lyutogo S 121 125 ISSN 0001 0782 DOI 10 1145 358396 358402 Why3 why3 lri fr originalu za 12 zhovtnya 2020 Procitovano 10 zhovtnya 2020 Alternative Provers SPARK User s Guide 22 0w docs adacore com originalu za 12 zhovtnya 2020 Procitovano 10 zhovtnya 2020 Bernard Carre Reliable programming in standard languages C T Sennett High Integrity Software Boston MA Springer US 1989 5 July P 102 121 ISBN 978 1 4684 5775 9 DOI 10 1007 978 1 4684 5775 9 5 Praxis and AdaCore Announce SPARK Pro AdaCore angl originalu za 21 veresnya 2020 Procitovano 10 zhovtnya 2020 Use of SPARK in a Certification Context The AdaCore Blog angl originalu za 12 zhovtnya 2020 Procitovano 10 zhovtnya 2020 LiteraturaJohn Barnes 2012 SPARK The Proven Approach to High Integrity Software Altran Praxis ISBN 978 0 9572905 1 8 Arhivovano zhovten 14 2016 na sajti 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 Barns Dzh Brasgol B Bezopasnoe i nadezhnoe programmnoe obespechenie na primere yazyka Ada 2012 SPARK 2014 2015 154 s Yannick Moy SPARK Ada for the MISRA C Developer 2019 PosilannyaStorinka SPARK Ada na sajti Ada Resource Association SPARK Pro SPARK Libre Arhivna kopiya na sajti Wayback Machine Dovidka zi SPARK 2014

Дата публікації:
Топ