| SZIKRA | |
|---|---|
| Nyelvóra | több paradigma |
| Megjelent | 1988 |
| Fejlesztő | Altran , AdaCore |
| Kiadás | 22 (2021 ) |
| Típusrendszer | statikus , szigorú , biztonságos , névelő |
| Főbb megvalósítások | SPARK Pro, SPARK GPL Edition |
| Befolyásolt | A pokolba , Eiffel |
| Engedély | GPLv3 |
| Weboldal | adaic.org/advantages/spa… |
| OS | Linux , Microsoft Windows , macOS |
A SPARK ( SPADE Ada Kernel [1] ) egy formálisan meghatározott programozási nyelv , amely az Ada [2] egy részhalmaza, és magas szintű biztonsági integritású ellenőrzött szoftverek fejlesztésére szolgál . A SPARK lehetővé teszi olyan alkalmazások létrehozását, amelyek kiszámítható viselkedésűek és nagy megbízhatóságot biztosítanak.
A SPARK nyelvi verziói az Ada verziókhoz kapcsolódnak, és két generációra oszthatók: a SPARK 83, a SPARK 95 és a SPARK 2005 (Ada 83, Ada 95 és Ada 2005) az első generációhoz, a SPARK 2014 (Ada 2012) pedig a másodikhoz tartozik. . Ez annak köszönhető, hogy kezdetben a megjegyzésekkel jelezték a specifikációkat és a szerződéseket , de 2012-től Ada-tól kezdődően erre a nyelvben megjelent szempontmechanizmust kezdték használni. Ez a teljes nyelvi eszköztár teljes újratervezéséhez és egy új GNATprove ellenőrző megjelenéséhez vezetett.
A SPARK-ot a repülésben ( Rolls-Royce Trent sugárhajtóművek [3] , Eurofighter Typhoon [4] és Be-200 [5] repülőgépek , UK NATS iFACTS rendszer [6] ) és űrrendszerek fejlesztésére használják ( Vega hordozórakéta , sok műhold [7] ). Titkosító rendszerek [8] és kiberbiztonság [9] [10] [11] fejlesztésére is használják .
A SPARK fejlesztés célja az volt, hogy megőrizze az Ada erősségeit (például a csomagrendszert és a korlátozott típusokat), és eltávolítson belőle minden potenciálisan nem biztonságos vagy félreérthető konstrukciót [1] , mivel az Ada a megfogalmazott fejlesztési célok ellenére egy meglehetősen összetett nyelv és nem rendelkezett teljes formális definíciókkal [1] , és egyes részei komoly kritikát váltottak ki [12] . A SPARK programok legyenek egyértelműek, viselkedésük ne függjön a fordítóprogramtól [K 1] , a fordítási lehetőségektől és a környezet állapotától. Ennek érdekében bizonyos korlátozásokat vezettek be a nyelvbe, többek között: a feladatok használata csak a Ravenscar profilban lehetséges; a kifejezések nem engednek mellékhatásokat ; tilos a vezérelt típusok használata, amelyekhez lehetőség van inicializálási eljárások újradefiniálására és operátor hozzárendelésére; a nevek kombinációja tilos; néhány operátor korlátozott használata, például a goto ; a dinamikus memóriafoglalás tilos (de dinamikus határokkal és diszkriminálókkal rendelkező típusok megengedettek) [2] .
Bármely SPARK programot azonban továbbra is le tudja fordítani az Ada fordító, amely lehetővé teszi ezeknek a nyelveknek a keverését egy projektben.
A SPARK fejlesztőinek sikerült megszerezniük az automatikus ellenőrzéshez kényelmes nyelvet, amely egyszerű szemantikával, szigorú formai definícióval, logikai helyességgel és jó kifejezőképességgel rendelkezik [1] .
Egy olyan eljáráshoz, amely valamely globális változó értékét az argumentumával növeli, ha az pozitív, és egyébként eggyel, a következő specifikációt írhatja fel:
eljárás Add_to_Total ( Érték : egész számban ) a következővel: Global => ( In_Out => Total ), Depends => ( Total => ( Total , Value )), Pre => ( Total < Integer ' Last - ( ha Érték > 0 , akkor Érték else 1 )), Post => ( Összesen = Összesen ' Régi + ( ha Érték > 0 , akkor Érték else 1 ));A Globális szempont megmutatja, hogy az eljárás mely globális változókhoz fér hozzá. Ebben az esetben csak az Összes változót használja olvasásra és írásra. A Depends a változók közötti kapcsolatot mutatja: a Total új értéke a régi értékétől és az Érték értékétől függ . Elő - előfeltétel, megmutatja, hogy a program milyen állapotban legyen az eljárás végrehajtása előtt; ebben az esetben az előfeltétel ellenőrzi, hogy nincs-e túlcsordulás. A Post utófeltétel, megmutatja a program állapotát az eljárás végrehajtása után.
A rutinok szempontjain kívül más módok is vannak a program állapotára vonatkozó korlátozások megadására, például ellenőrző utasítások:
pragma Assert ( Feltétel );vagy ciklusinvariánsok:
pragma Loop_Invariant ( Feltétel );Ugyanakkor jelentős különbségek vannak a szerződések leírásának szintaxisában az első és második generációs SPARK verziók esetében.
A nyelv első generációja speciális megjegyzéseket használt:
-- Természetes szám megkettőzése. eljárás Dupla ( X : in out Natural ); --# pre X < Natural'Last / 2; --# post X = 2 * X~;Egyenértékű kód a második generációhoz:
-- Természetes szám megkettőzése. eljárás Dupla ( X : in out Natural ) with Pre => X < Natural ' Last / 2 , Post => X = 2 * X ' Old ;A programok ellenőrzésekor a következő módszereket kell használni:
A program helyességének bizonyítására a programozó által használt összes konstrukcióhoz, mint például az elő- és utófeltételekhez ellenőrző utasításkészletek készülnek. A GNATprove ellenőrző bizonyos esetekben önmagában is képes hitelesítési állításokat generálni. Tehát a tömbök vagy típusok határain túllépések, a túlcsordulás és a nullával való osztás ellenőrzése megtörténik.
Továbbá egy sor ellenőrző nyilatkozat és a program kezdeti állapotára vonatkozó adatok, valamint a fejlesztőtől kapott ellenőrizhetetlen nyilatkozatok átkerülnek az automatikus ellenőrző programba. A GNATprove a Why3 platformot [13] és a CVC4, Z3 és Alt-Ergo [14] tesztellenőrző rendszereket használja . Harmadik féltől származó rendszerek, mint például a Coq [14] , szintén használhatók bizonyításra .
A SPARK első verzióját (Ada 83 alapján) a Southamptoni Egyetemen hozták létre a brit védelmi minisztérium támogatásával Bernard Carré és Trevor Jennings , a SPADE-Pascal [15] megbízható Pascal programozási rendszer szerzői . Továbbá a következő cégek dolgoztak a nyelv fejlesztésén: Program Validation Limited, Praxis Critical Systems Limited (a továbbiakban Altran-Praxis, Altran) és AdaCore.
2009 elején a Praxis megállapodást kötött az AdaCore-ral, és kiadta a SPARK Pro-t a GPL feltételei szerint [16] . Aztán 2009 júniusában megjelent a SPARK GPL Edition, amelynek célja az ingyenes és tudományos szoftverfejlesztés.
A SPARK 2014 második generációs nyelvi verziójának megjelenését 2014. április 30-án jelentették be [17] .
Hozzászólások
Források