SPARK (język programowania) - SPARK (programming language)
Paradygmat | Wieloparadygmat |
---|---|
Deweloper | Altran i AdaCore |
Wersja stabilna | Wspólnota 2021 / 1 czerwca 2021
|
Dyscyplina pisania | statyczny , mocny , bezpieczny , mianownik |
OS | Wieloplatformowy : Linux , Microsoft Windows , Mac OS X |
Licencja | GPLv3 |
Strona internetowa | O SPARK |
Główne wdrożenia | |
SPARK Pro, SPARK GPL Edition, Społeczność SPARK | |
Wpływem | |
Ada , Eiffel |
SPARK to formalnie zdefiniowany język programowania komputerowego oparty na języku programowania Ada , przeznaczony do tworzenia oprogramowania o wysokiej integralności stosowanego w systemach, w których kluczowe znaczenie ma przewidywalne i wysoce niezawodne działanie. Ułatwia tworzenie aplikacji wymagających bezpieczeństwa, ochrony lub integralności biznesowej.
Pierwotnie istniały trzy wersje języka SPARK (SPARK83, SPARK95, SPARK2005) oparte odpowiednio na Ada 83, Ada 95 i Ada 2005.
Czwarta wersja języka SPARK, SPARK 2014, oparta na Ada 2012, została wydana 30 kwietnia 2014 r. SPARK 2014 to całkowite przeprojektowanie języka i wspierające narzędzia weryfikacyjne .
Język SPARK składa się z dobrze zdefiniowanego podzbioru języka Ada, który używa kontraktów do opisywania specyfikacji komponentów w formie, która jest odpowiednia zarówno do weryfikacji statycznej, jak i dynamicznej.
W SPARK83/95/2005 kontrakty są kodowane w komentarzach Ady i dlatego są ignorowane przez każdy standardowy kompilator Ada, ale są przetwarzane przez SPARK „Examiner” i powiązane z nim narzędzia.
W przeciwieństwie do tego SPARK 2014 wykorzystuje wbudowaną składnię „aspektową” Ada 2012 do wyrażania umów, przenosząc je do rdzenia języka. Główne narzędzie SPARK 2014 (GNATprove) opiera się na infrastrukturze GNAT/GCC i wykorzystuje prawie cały front-end GNAT Ada 2012.
Przegląd techniczny
SPARK wykorzystuje mocne strony Ady, starając się wyeliminować wszystkie jej potencjalne niejasności i niepewne konstrukcje. Programy SPARK są z założenia jednoznaczne, a na ich zachowanie nie ma wpływu wybór kompilatora Ada . Cele te są osiągane częściowo przez pominięcie niektórych bardziej problematycznych funkcji Ady (takich jak nieograniczone równoległe wykonywanie zadań ), a częściowo poprzez wprowadzenie kontraktów, które kodują intencje projektanta aplikacji i wymagania dotyczące określonych składników programu.
Połączenie tych podejść pozwala SPARK osiągnąć swoje cele projektowe, którymi są:
- logiczny rozsądek
- rygorystyczna definicja formalna
- prosta semantyka
- bezpieczeństwo
- siła wyrazu
- Sprawdzalność
- ograniczone wymagania dotyczące zasobów (miejsca i czasu).
- minimalne wymagania systemowe środowiska uruchomieniowego
Przykłady umów
Rozważ poniższą specyfikację podprogramu Ada:
procedure Increment (X : in out Counter_Type);
W czystej Adzie może to zwiększyć zmienną X
o jeden lub tysiąc; lub może ustawić jakiś globalny licznik na X
i zwrócić oryginalną wartość licznika w X
; albo może w ogóle nic nie robić X
.
W SPARK 2014 do kodu są dodawane kontrakty, aby zapewnić dodatkowe informacje dotyczące tego, co faktycznie robi podprogram. Na przykład możemy zmienić powyższą specyfikację, aby powiedzieć:
procedure Increment (X : in out Counter_Type) with Global => null, Depends => (X => X);
Określa to, że Increment
procedura nie używa (ani aktualizuje, ani nie odczytuje) żadnej zmiennej globalnej i że jedynym elementem danych używanym do obliczania nowej wartości X
jest ona X
sama.
Alternatywnie projektant może określić:
procedure Increment (X : in out Counter_Type) with Global => (In_Out => Count), Depends => (Count => (Count, X), X => null);
Oznacza to, że Increment
użyje zmiennej globalnej Count
w tym samym pakiecie co Increment
, że eksportowana wartość Count
zależy od importowanych wartości Count
i X
oraz że eksportowana wartość X
nie zależy w ogóle od żadnej zmiennej i będzie wyprowadzona tylko z danych stałych .
Jeśli GNATprove zostanie następnie uruchomiony na specyfikacji i odpowiadającej jej treści podprogramu, przeanalizuje treść podprogramu, aby zbudować model przepływu informacji. Ten model jest następnie porównywany z modelem, który został określony przez adnotacje i wszelkie rozbieżności zgłoszone użytkownikowi.
Specyfikacje te mogą być dalej rozszerzone przez zapewnienie różnych właściwości, które albo muszą być zachowane, gdy podprogram jest wywoływany ( warunki wstępne ), albo które będą zachowane po zakończeniu wykonywania podprogramu (warunki końcowe ). Na przykład moglibyśmy powiedzieć, co następuje:
procedure Increment (X : in out Counter_Type) with Global => null, Depends => (X => X), Pre => X < Counter_Type'Last, Post => X = X'Old + 1;
To teraz określa nie tylko, że X
wywodzi się z samego siebie, ale także, że przed Increment
wywołaniem X
musi być ściśle mniejsza niż ostatnia możliwa wartość tego typu i że później X
będzie równa początkowej wartości X
plus jeden.
Warunki weryfikacji
GNATprove może również generować zestaw warunków weryfikacji lub VC. Warunki te służą do ustalenia, czy dla danego podprogramu obowiązują pewne właściwości. Jako minimum, GNATprove wygeneruje VC w celu ustalenia, że wszystkie błędy czasu wykonania nie mogą wystąpić w podprogramie, takie jak:
- indeks tablicy poza zakresem
- wpisz naruszenie zakresu
- dzielenie przez zero
- przepełnienie liczbowe.
Jeśli do podprogramu zostanie dodany warunek końcowy lub jakiekolwiek inne potwierdzenie, GNATprove wygeneruje również VC, które wymagają od użytkownika wykazania, że te właściwości obowiązują dla wszystkich możliwych ścieżek w podprogramie.
Pod maską GNATprove wykorzystuje język pośredni Why3 i generator VC, a do rozładowywania VC udowodniono twierdzenia CVC4, Z3 i Alt-Ergo. Korzystanie z innych programów udowadniających (w tym interaktywnych programów sprawdzających dowody) jest również możliwe dzięki innym komponentom zestawu narzędzi Why3.
Historia
Pierwsza wersja SPARK (oparta na Ada 83) została wyprodukowana na Uniwersytecie w Southampton (przy wsparciu Ministerstwa Obrony Wielkiej Brytanii ) przez Bernarda Carré i Trevora Jenningsa. Nazwa SPARK pochodzi od jądra SPADE Ada , w odniesieniu do podzbioru SPADE języka programowania Pascal .
Następnie język był stopniowo rozszerzany i udoskonalany, najpierw przez Program Validation Limited, a następnie przez Praxis Critical Systems Limited. W 2004 roku Praxis Critical Systems Limited zmieniła nazwę na Praxis High Integrity Systems Limited. W styczniu 2010 roku firma zmieniła nazwę na Altran Praxis .
Na początku 2009 roku Praxis nawiązała współpracę z AdaCore i wydała „SPARK Pro” na warunkach GPL. Następnie w czerwcu 2009 wydano SPARK GPL Edition 2009, skierowaną do FOSS i środowisk akademickich.
W czerwcu 2010 r. Altran-Praxis ogłosił, że język programowania SPARK będzie używany w oprogramowaniu amerykańskiego projektu Lunar CubeSat , którego ukończenie ma się zakończyć w 2015 r.
W styczniu 2013 roku Altran-Praxis zmieniło nazwę na Altran.
Pierwsze wydanie PRO SPARK 2014 zostało ogłoszone 30 kwietnia 2014 r., a wkrótce potem pojawiła się edycja SPARK 2014 GPL, skierowana do społeczności FLOSS i środowisk akademickich.
Zastosowania przemysłowe
SPARK był stosowany w kilku wysokoprofilowych systemach krytycznych dla bezpieczeństwa, obejmujących lotnictwo komercyjne ( silniki odrzutowe serii Rolls-Royce Trent , system ARINC ACAMS, Lockheed Martin C130J), lotnictwo wojskowe ( EuroFighter Typhoon , Harrier GR9, AerMacchi M346), lotnictwo -zarządzanie ruchem (system UK NATS iFACTS), koleją (liczne aplikacje sygnalizacyjne), medycyną ( urządzenie wspomagające pracę komór LifeFlow ) i zastosowaniami kosmicznymi (projekt Vermont Technical College CubeSat ).
SPARK został również wykorzystany do tworzenia bezpiecznych systemów. Wśród użytkowników są Rockwell Collins (rozwiązania międzydomenowe Turnstile i SecureOne), rozwój oryginalnego MULTOS CA, demonstrator NSA Tokeneer, wielopoziomowa stacja robocza secunet, jądro separacji Muen i szyfrator urządzeń blokowych Genode.
W sierpniu 2010 roku Rod Chapman, główny inżynier Altran Praxis, wdrożył Skeina , jednego z kandydatów na SHA-3 , w firmie SPARK. Porównując wydajność implementacji SPARK i C i po starannej optymalizacji, udało mu się uruchomić wersję SPARK tylko o około 5 do 10% wolniej niż C. Późniejsze ulepszenie środkowej części Ady w GCC (wdrożone przez Erica Botcazou z AdaCore ) wypełnił lukę, a kod SPARK dokładnie pasował do C pod względem wydajności.
NVIDIA zastosowała również SPARK do implementacji oprogramowania układowego o znaczeniu krytycznym dla bezpieczeństwa.
W 2020 roku Rod Chapman ponownie zaimplementował bibliotekę kryptograficzną TweetNaCl w SPARK 2014. Wersja SPARK biblioteki ma pełny autoaktywny dowód bezpieczeństwa typu, bezpieczeństwa pamięci i niektórych właściwości poprawności, a także zachowuje algorytmy czasu stałego przez cały czas. Kod SPARK jest również znacznie szybszy niż TweetNaCl.
Zobacz też
Bibliografia
Dalsza lektura
- Johna Barnesa (2012). SPARK: Sprawdzone podejście do oprogramowania o wysokiej integralności . Praxis Altran. Numer ISBN 978-0-9572905-1-8.
- John W. McCormick i Peter C. Chapin (2015). Tworzenie aplikacji o wysokiej integralności za pomocą SPARK 2014 . Wydawnictwo Uniwersytetu Cambridge. Numer ISBN 978-1-107-65684-0.
- Philip E. Ross (wrzesień 2005). „Tępiciele” . Widmo IEEE . 42 (9): 36–41. doi : 10.1109/MSPEC.2005.1502527 . ISSN 0018-9235 .
Zewnętrzne linki
- Strona społeczności SPARK 2014
- Strona internetowa SPARK Pro
- Witryna internetowa edycji SPARK Libre (GPL)
- Altran
- Poprawność według konstrukcji: manifest oprogramowania o wysokiej integralności
- Brytyjski klub systemów krytycznych dla bezpieczeństwa
- Porównanie z językiem specyfikacji C (Frama C)
- Strona projektu Tokeneera
- Publikacja publiczna jądra Muen
- Projekt LifeFlow LVAD
- Projekt VTU CubeSat