| GNISTA | |
|---|---|
| Språkklass | multiparadigm |
| Framträdde i | 1988 |
| Utvecklaren | Altran , AdaCore |
| Släpp | 22 (2021 ) |
| Typ system | statisk , strikt , säker , nominativ |
| Stora implementeringar | SPARK Pro, SPARK GPL Edition |
| Blivit påverkad | Helvete , Eiffel |
| Licens | GPLv3 |
| Hemsida | adaic.org/advantages/spa... |
| OS | Linux , Microsoft Windows , macOS |
SPARK ( SPADE Ada Kernel [1] ) är ett formellt definierat programmeringsspråk , som är en delmängd av Ada [2] , designat för att utveckla verifierad programvara med hög säkerhetsintegritet . SPARK låter dig skapa applikationer som har förutsägbart beteende och ger hög tillförlitlighet.
SPARK språkversioner är relaterade till Ada-versioner och är uppdelade i två generationer: SPARK 83, SPARK 95 och SPARK 2005 (Ada 83, Ada 95 respektive Ada 2005) tillhör den första generationen och SPARK 2014 (Ada 2012) till den andra . Detta beror på det faktum att kommentarer från början användes för att ange specifikationer och kontrakt , men från och med Ada 2012 började aspektmekanismen som dök upp i språket att användas för detta. Detta ledde till en fullständig omdesign av hela språkverktygslådan och uppkomsten av en ny GNATprove-verifierare.
SPARK används inom flyg ( Rolls-Royce Trent jetmotorer [3] , Eurofighter Typhoon [4] och Be-200 [5] flygplan , UK NATS iFACTS system [6] ) och för utveckling av rymdsystem ( Vega launch vehicle , många satelliter [7 ] ). Det används också för att utveckla krypteringssystem [8] och cybersäkerhet [9] [10] [11] .
Målet med SPARK-utvecklingen var att bevara styrkorna hos Ada (som paketsystemet och begränsade typer) och ta bort alla potentiellt osäkra eller tvetydiga konstruktioner från det [1] , eftersom Ada, trots de angivna utvecklingsmålen, visade sig vara en ganska komplext språk och hade inte en fullständig formell definition [1] , och några av dess delar har orsakat allvarlig kritik [12] . SPARK-program bör vara entydiga, deras beteende bör inte bero på valet av kompilator [K 1] , kompileringsalternativ och miljöns tillstånd. För att göra detta har vissa begränsningar införts i språket, inklusive: användningen av uppgifter är endast möjlig i Ravenscar-profilen; uttryck tillåter inte biverkningar ; det är förbjudet att använda kontrollerade typer, för vilka det är möjligt att omdefiniera initieringsprocedurer och tilldelningsoperatör; kombination av namn är förbjuden; begränsad användning av vissa operatörer som goto ; dynamisk minnesallokering är förbjuden (men typer med dynamiska gränser och typer med diskriminanter är tillåtna) [2] .
Alla SPARK-program kan dock fortfarande kompileras av Ada-kompilatorn, som låter dig blanda dessa språk i ett projekt.
SPARK-utvecklarna lyckades få ett språk som är bekvämt för automatisk verifiering, som har enkel semantik, en strikt formell definition, logisk korrekthet och bra uttrycksförmåga [1] .
För en procedur som ökar värdet på en global variabel med dess argument om den är positiv, och med en annars, kan du skriva följande specifikation:
procedur Add_to_Total ( Value : in Heltal ) med Global => ( In_Out => Total ), Depends => ( Total => ( Total , Value )), Pre => ( Totalt < Integer ' Last - ( om Värde > 0 då värde else 1 )), Post => ( Totalt = Totalt ' Old + ( om Värde > 0 då Värde annat 1 ));Global aspekten visar vilka globala variabler proceduren har tillgång till. I det här fallet använder den bara variabeln Total för att läsa och skriva. Depends visar förhållandet mellan variabler: det nya värdet på Total beror på dess gamla värde och värdet på Value . Förutsättning - en förutsättning, det visar vilket tillstånd av programmet bör vara innan förfarandet utförs; i detta fall kontrollerar förutsättningen om ett spill inträffar. Post är ett eftervillkor, det visar programmets tillstånd efter att proceduren har utförts.
Utöver aspekter av rutiner finns det andra sätt att specificera begränsningar för ett programs tillstånd, till exempel kontrollera uttalanden:
pragma hävda ( tillstånd );eller loopinvarianter:
pragma Loop_Invariant ( villkor );Samtidigt finns det betydande skillnader i syntaxen för att beskriva kontrakt för SPARK-versionerna av första och andra generationen.
Den första generationen av språket använde speciella kommentarer:
-- Dubbla ett naturligt tal. procedur Dubbel ( X : in ut Naturlig ); --# pre X < Natural'Last / 2; --# post X = 2 * X~;Motsvarande kod för andra generationen:
-- Dubbla ett naturligt tal. procedur Dubbel ( X : in ut Naturlig ) med Pre => X < Natural ' Last / 2 , Post => X = 2 * X ' Old ;Vid verifiering av program används följande metoder:
För att bevisa programmets riktighet skapas uppsättningar av verifieringssatser för alla konstruktioner som används av programmeraren, såsom pre- och postconditions. GNATprove-verifieraren kan också, i vissa fall, generera verifieringspåståenden på egen hand. Så, kontroller för out of bounds of arrays eller typer, overflow och division med noll kommer att utföras.
Vidare överförs en uppsättning verifieringsutlåtanden och data om programmets initiala tillstånd, såväl som icke verifierbara uttalanden som tagits emot från utvecklaren, till det automatiska bevisprogrammet. GNATprove använder Why3-plattformen [13] och CVC4, Z3 och Alt-Ergo [14] testsäkra system . Tredjepartssystem som Coq [14] kan också användas för bevis .
Den första versionen av SPARK (baserad på Ada 83) skapades vid University of Southampton med stöd av det brittiska försvarsministeriet av Bernard Carré och Trevor Jennings , författare till det pålitliga programmeringssystemet SPADE-Pascal [15] Pascal . Vidare arbetade följande företag med att förbättra språket: Program Validation Limited, Praxis Critical Systems Limited (nedan kallat Altran-Praxis, Altran) och AdaCore.
I början av 2009 ingick Praxis ett avtal med AdaCore och släppte SPARK Pro under villkoren i GPL [16] . Sedan i juni 2009 släpptes SPARK GPL Edition, som syftar till gratis och akademisk mjukvaruutveckling.
Utgivningen av den andra generationens språkversion SPARK 2014 tillkännagavs den 30 april 2014 [17] .
Kommentarer
Källor