SPARK (programming language)

rdf:langString SPARK (informatyka)

rdf:langString SPARK Ada, SPARK 95 – podzbiór języka Ada zaprojektowany w celu tworzenia kodu wolnego od błędów dla zastosowania w systemach mission-critical. Język został stworzony w 1999 roku przez brytyjską firmę na bazie podobnego podzbioru języka SPADE Pascal oraz języka Ada 95. Język jest zaprojektowany w taki sposób, aby możliwa była formalna analiza oraz dowodzenie poprawności kodu. Usunięte zostały z niego wszelkie dwuznaczności, elementy sprzyjające nieprzewidzianym przepływom danych (np. wyjątki), wprowadzono mechanizm formalnych komentarzy (formal comments, annotations). W celu umożliwienia silnej weryfikacji poprawności kodu wprowadzono precyzyjne specyfikacje wejścia i wyjścia poszczególnych procedur. Ochronę stabilności zapewnia m.in. wewnętrzna kontrola liczby iteracji oraz czasu wykonania procedur. Język posiada szereg rozszerzeń przeznaczonych do obsługi urządzeń fizycznych działających w czasie rzeczywistym np. sensorów. Programy napisane w języku SPARK Ada są kompatybilne ze standardowym językiem Ada. Funkcje formalnej analizy poprawności są relizowane przez dodatkowe narzędzia (SPARK Examiner) bazujące głównie na rozszerzeniach jakimi są formalne komentarze. Przykład fragmentu kodu z formalnymi komentarzami SPARK: procedure Increment (X : in out Counter_Type);--# derives X from X;--# pre X < Counter_Type'Last;--# post X = X~ + 1; Komentarze te precyzyjnie określają do jakich zmiennych globalnych odwołuje się dana funkcja oraz w jaki sposób wpływa ona na wartość zmiennej X (może być tylko większa o 1, nie mniejsza, ani nie równa początkowej wartości) oraz jaka musi być początkowa wartość zmiennej X (mniejsza od największej dopuszczalnej wartości Counter_Type). Deklaracje te stanowią podstawę dla formalnej weryfikacji kodu funkcji przez SPARK Examiner, który sprawdza czy wynik działania tego kodu będzie zgodny z deklaracjami formalnymi.