Redakcja
Choć brzmi to jak mrzonka, jest to prawda. Stworzono tak złożony język, że nie trzeba go testować... i ma on już 10 lat.
Język SPARK jest pochodną języka Ada i jego założeniem jest, że sam wspiera weryfikację swojej funkcjonalności. Używany jest między innymi do budowanie aplikacji wbudowanych od których może zależeć ludzkie życie takich jak sprzęt lotniczy, medyczny czy systemy kontroli reaktorów jądrowych.
Z kodu usunięto wszelkie dwuznaczności oraz elementy sprzyjające nieprzewidzianym przepływom jak np. wyjątki. 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 (za Wikipedia).
