| JISKRA | |
|---|---|
| Jazyková třída | multi-paradigma |
| Objevil se v | 1988 |
| Vývojář | Altran , AdaCore |
| Uvolnění | 22 (2021 ) |
| Typový systém | statický , přísný , bezpečný , nominativní |
| Hlavní implementace | SPARK Pro, SPARK GPL Edition |
| Byl ovlivněn | Sakra , Eiffeli |
| Licence | GPLv3 |
| webová stránka | adaic.org/advantages/spa… |
| OS | Linux , Microsoft Windows , macOS |
SPARK ( SPADE Ada Kernel [1] ) je formálně definovaný programovací jazyk , který je podmnožinou Ada [2] , určený k vývoji ověřeného softwaru s vysokou úrovní integrity bezpečnosti . SPARK vám umožňuje vytvářet aplikace, které mají předvídatelné chování a poskytují vysokou spolehlivost.
Jazykové verze SPARK souvisí s verzemi Ada a jsou rozděleny do dvou generací: SPARK 83, SPARK 95 a SPARK 2005 (Ada 83, Ada 95 a Ada 2005) patří do první generace a SPARK 2014 (Ada 2012) do druhé. . Důvodem je skutečnost, že zpočátku byly k označení specifikací a smluv použity komentáře , ale počínaje Adou 2012 se k tomu začal používat mechanismus aspektů, který se objevil v jazyce. To vedlo ke kompletnímu přepracování celé sady jazykových nástrojů a ke vzniku nového ověřovače GNATprove.
SPARK se používá v letectví ( proudové motory Rolls-Royce Trent [3] , letouny Eurofighter Typhoon [4] a Be-200 [5] , UK NATS systém iFACTS [6] ) a pro vývoj vesmírných systémů ( nosná raketa Vega , mnoho satelitů [7 ] ). Používá se také k vývoji šifrovacích systémů [8] a kybernetické bezpečnosti [9] [10] [11] .
Cílem vývoje SPARK bylo zachovat silné stránky Ada (jako je systém balíčků a omezené typy) a odstranit z něj všechny potenciálně nebezpečné nebo nejednoznačné konstrukty [1] , protože Ada se navzdory uvedeným vývojovým cílům ukázala jako poměrně složitý jazyk a neměl kompletní formální definice [1] a některé jeho části vyvolaly vážnou kritiku [12] . Programy SPARK by měly být jednoznačné, jejich chování by nemělo záviset na volbě kompilátoru [K 1] , možnostech kompilace a stavu prostředí. Za tímto účelem byla do jazyka zavedena některá omezení, včetně: použití úkolů je možné pouze v profilu Ravenscar; výrazy neumožňují vedlejší účinky ; je zakázáno používat řízené typy, u kterých je možné předefinovat inicializační procedury a operátor přiřazení; kombinace jmen je zakázána; omezené použití některých operátorů, jako je goto ; dynamická alokace paměti je zakázána (ale typy s dynamickými hranicemi a typy s diskriminanty jsou povoleny) [2] .
Jakýkoli program SPARK však může být stále zkompilován kompilátorem Ada, který vám umožňuje kombinovat tyto jazyky v jednom projektu.
Vývojářům SPARK se podařilo získat jazyk vhodný pro automatické ověřování, který má jednoduchou sémantiku, přísnou formální definici, logickou správnost a dobrou expresivitu [1] .
Pro proceduru, která zvyšuje hodnotu nějaké globální proměnné o její argument, pokud je kladná, a o jedničku jinak, můžete napsat následující specifikaci:
procedura 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 ));Aspekt Globální ukazuje, ke kterým globálním proměnným má procedura přístup. V tomto případě pro čtení a zápis používá pouze proměnnou Total . Depends ukazuje vztah mezi proměnnými: nová hodnota Total závisí na jeho staré hodnotě a hodnotě Value . Předběžná podmínka, ukazuje, v jakém stavu by měl být program před provedením procedury; v tomto případě předběžná podmínka zkontroluje, zda nedošlo k přetečení. Post je postcondition, ukazuje stav programu po provedení procedury.
Kromě aspektů rutin existují další způsoby, jak určit omezení stavu programu, jako jsou kontrolní příkazy:
pragma Assert ( Stav );nebo smyčkové invarianty:
pragma Loop_Invariant ( Podmínka );Zároveň existují značné rozdíly v syntaxi popisu smluv pro verze SPARK první a druhé generace.
První generace jazyka používala speciální komentáře:
-- Zdvojnásobení přirozeného čísla. procedure Double ( X : in out Natural ); --# pre X < Natural'Last / 2; --# příspěvek X = 2 * X~;Ekvivalentní kód pro druhou generaci:
-- Zdvojnásobení přirozeného čísla. procedura Double ( X : in out Natural ) with Pre => X < Natural ' Last / 2 , Post => X = 2 * X ' Old ;Při ověřování programů se používají následující metody:
Aby se prokázala správnost programu, pro všechny konstrukty používané programátorem, jako jsou pre- a postconditions, jsou vytvořeny sady ověřovacích příkazů. Verifikátor GNATprove může také v některých případech generovat ověřovací tvrzení sám. Takže budou provedeny kontroly mimo hranice polí nebo typů, přetečení a dělení nulou.
Dále je do programu automatického nátisku přenesena sada ověřovacích výpisů a dat o počátečním stavu programu a také neověřitelné výpisy obdržené od vývojáře. GNATprove používá platformu Why3 [13] a testovací systémy CVC4, Z3 a Alt-Ergo [14] . Pro důkaz lze také použít systémy třetích stran, jako je Coq [14] .
První verze SPARK (založená na Ada 83) byla vytvořena na University of Southampton s podporou britského ministerstva obrany Bernardem Carré a Trevorem Jenningsem , autory spolehlivého programovacího systému SPADE-Pascal [15] Pascal . Dále na vylepšení jazyka pracovaly tyto společnosti: Program Validation Limited, Praxis Critical Systems Limited (dále Altran-Praxis, Altran) a AdaCore.
Začátkem roku 2009 Praxis uzavřel smlouvu s AdaCore a vydal SPARK Pro za podmínek GPL [16] . V červnu 2009 byla vydána SPARK GPL Edition, zaměřená na vývoj svobodného a akademického softwaru.
Vydání druhé generace jazykové verze SPARK 2014 bylo oznámeno 30. dubna 2014 [17] .
Komentáře
Prameny