| KIPINÄ | |
|---|---|
| Kieliluokka | moniparadigma |
| Esiintyi | 1988 |
| Kehittäjä | Altran , AdaCore |
| Vapauta | 22 (2021 ) |
| Tyyppijärjestelmä | staattinen , tiukka , turvallinen , nimeävä |
| Tärkeimmät toteutukset | SPARK Pro, SPARK GPL Edition |
| Vaikutettu | Helvetti , Eiffel |
| Lisenssi | GPLv3 |
| Verkkosivusto | adaic.org/advantages/spa… |
| OS | Linux , Microsoft Windows , macOS |
SPARK ( SPADE Ada Kernel [1] ) on muodollisesti määritelty ohjelmointikieli , joka on Adan [2] osajoukko, joka on suunniteltu kehittämään varmennettuja ohjelmistoja, joilla on korkea turvallisuustaso . SPARKin avulla voit luoda sovelluksia, joilla on ennakoitavissa oleva toiminta ja korkea luotettavuus.
SPARK-kieliversiot liittyvät Adan versioihin ja on jaettu kahteen sukupolveen: SPARK 83, SPARK 95 ja SPARK 2005 (vastaavasti Ada 83, Ada 95 ja Ada 2005) kuuluvat ensimmäiseen sukupolveen ja SPARK 2014 (Ada 2012) toiseen sukupolveen. . Tämä johtuu siitä, että alun perin kommentteja käytettiin osoittamaan eritelmiä ja sopimuksia , mutta Ada 2012:sta lähtien tähän alettiin käyttää kieleen ilmestynyttä aspektimekanismia. Tämä johti koko kielityökalupaketin täydelliseen uudelleensuunnitteluun ja uuden GNATprove-todentajan syntymiseen.
SPARKia käytetään ilmailussa ( Rolls-Royce Trent -suihkumoottorit [3] , Eurofighter Typhoon [4] ja Be-200 [5] lentokoneet , UK NATS iFACTS -järjestelmä [6] ) ja avaruusjärjestelmien kehittämiseen ( Vega kantoraketti , monet satelliitit [7 ] ). Sitä käytetään myös salausjärjestelmien [8] ja kyberturvallisuuden [9] [10] [11] kehittämiseen .
SPARK-kehityksen tavoitteena oli säilyttää Adan vahvuudet (kuten pakettijärjestelmä ja rajoitetut tyypit) ja poistaa siitä kaikki mahdollisesti vaaralliset tai epäselvät rakenteet [1] , koska Ada, ilmoitetuista kehitystavoitteista huolimatta, osoittautui melko monimutkaista kieltä, eikä sillä ollut täydellisiä muodollisia määritelmiä [1] , ja jotkut sen osat ovat aiheuttaneet vakavaa kritiikkiä [12] . SPARK-ohjelmien tulee olla yksiselitteisiä, niiden käyttäytyminen ei saa riippua kääntäjän valinnasta [K 1] , käännösvaihtoehdoista ja ympäristön tilasta. Tätä varten kieleen on lisätty joitain rajoituksia, mukaan lukien: tehtävien käyttö on mahdollista vain Ravenscar-profiilissa; ilmaukset eivät salli sivuvaikutuksia ; on kiellettyä käyttää ohjattuja tyyppejä, joille on mahdollista määritellä uudelleen alustusmenettelyt ja osoitusoperaattori; nimien yhdistäminen on kielletty; joidenkin operaattoreiden, kuten goto , rajoitettu käyttö ; dynaaminen muistin varaus on kielletty (mutta tyypit, joissa on dynaamiset rajat ja tyypit, joissa on erotteita, ovat sallittuja) [2] .
Ada-kääntäjä voi kuitenkin edelleen kääntää minkä tahansa SPARK-ohjelman, jonka avulla voit sekoittaa nämä kielet yhteen projektiin.
SPARK-kehittäjät onnistuivat saamaan automaattiseen todentamiseen sopivan kielen, jolla on yksinkertainen semantiikka, tiukka muodollinen määritelmä, looginen oikeellisuus ja hyvä ilmaisukyky [1] .
Proseduurille, joka kasvattaa jonkin globaalin muuttujan arvoa argumentillaan, jos se on positiivinen, ja muussa tapauksessa yhdellä, voit kirjoittaa seuraavan määrityksen:
menettely Add_to_Total ( Arvo : kokonaislukuna ) ja Global => ( In_Out => Total ), Depends => ( Total => ( Total , Value )), Pre = > ( Total < Integer ' Last - ( jos Arvo > 0 niin arvo else 1 )), Viesti => ( Yhteensä = Yhteensä ' Vanha + ( jos Arvo > 0 niin Arvo else 1 ));Globaali - aspekti näyttää, mihin globaaleihin muuttujiin menettelyllä on pääsy. Tässä tapauksessa se käyttää vain Total -muuttujaa lukemiseen ja kirjoittamiseen. Riippuu näyttää muuttujien välisen suhteen: Totalin uusi arvo riippuu sen vanhasta arvosta ja Arvon arvosta . Ennakkoehto , se näyttää, mikä tila ohjelman tulee olla ennen toimenpiteen suorittamista; tässä tapauksessa ennakkoehto tarkistaa, tapahtuuko ylivuotoa. Postitus on jälkiehto , se näyttää ohjelman tilan toimenpiteen suorittamisen jälkeen.
Rutiinien lisäksi on muita tapoja määrittää ohjelman tilan rajoituksia, kuten tarkistuslausekkeita:
pragma Assert ( kunto );tai silmukkainvariantteja:
pragma Loop_Invariant ( ehto );Samanaikaisesti ensimmäisen ja toisen sukupolven SPARK-versioiden sopimusten kuvauksen syntaksissa on merkittäviä eroja.
Kielen ensimmäinen sukupolvi käytti erityisiä kommentteja:
-- Luonnollisen luvun kaksinkertaistaminen. menettely Double ( X : in out Natural ); --# pre X < Natural'Last / 2; --# viesti X = 2 * X~;Vastaava koodi toiselle sukupolvelle:
-- Luonnollisen luvun kaksinkertaistaminen. menettely Tupla ( X : in out Natural ) Pre => X < Natural ' Last / 2 , Post = > X = 2 * X ' Old ;Ohjelmia tarkistettaessa käytetään seuraavia menetelmiä:
Ohjelman oikeellisuuden todistamiseksi kaikille ohjelmoijan käyttämille rakenteille, kuten esi- ja jälkiehdolle, luodaan joukot varmennuslausekkeita. GNATprove-todentaja voi myös joissain tapauksissa luoda varmistusvahvistuksia itsekseen. Joten taulukoiden tai tyyppien rajojen ulkopuolella, ylivuoto ja nollalla jakaminen tarkistetaan.
Lisäksi automaattiseen tarkistusohjelmaan siirretään joukko varmennuslausuntoja ja tietoja ohjelman alkutilasta sekä kehittäjältä saadut varmentamattomat lausunnot. GNATprove käyttää Why3-alustaa [13] sekä CVC4-, Z3- ja Alt-Ergo [14] -testausjärjestelmiä . Todistukseen voidaan käyttää myös kolmannen osapuolen järjestelmiä, kuten Coq [14] .
SPADE-Pascalin [15] luotettavan Pascal -ohjelmointijärjestelmän kirjoittajat Bernard Carré ja Trevor Jennings loivat ensimmäisen SPARK-version (perustuu Ada 83:een) Southamptonin yliopistossa Britannian puolustusministeriön tuella . Lisäksi seuraavat yritykset työskentelivät kielen parantamiseksi: Program Validation Limited, Praxis Critical Systems Limited (jäljempänä Altran-Praxis, Altran) ja AdaCore.
Vuoden 2009 alussa Praxis solmi sopimuksen AdaCoren kanssa ja julkaisi SPARK Pron GPL :n ehtojen mukaisesti [16] . Sitten kesäkuussa 2009 julkaistiin SPARK GPL Edition, joka oli tarkoitettu ilmaiseen ja akateemiseen ohjelmistokehitykseen.
Toisen sukupolven kieliversion SPARK 2014 julkaisu julkistettiin 30. huhtikuuta 2014 [17] .
Kommentit
Lähteet