b"\n_START_ARTICLE_\nSPARK (informatyka)\n_START_PARAGRAPH_\nSPARK Ada, SPARK 95 \xe2\x80\x93 podzbi\xc3\xb3r j\xc4\x99zyka Ada zaprojektowany w celu tworzenia kodu wolnego od b\xc5\x82\xc4\x99d\xc3\xb3w dla zastosowania w systemach mission-critical._NEWLINE_J\xc4\x99zyk zosta\xc5\x82 stworzony w 1999 roku przez brytyjsk\xc4\x85 firm\xc4\x99 Praxis High Integrity Systems na bazie podobnego podzbioru j\xc4\x99zyka SPADE Pascal oraz j\xc4\x99zyka Ada 95. J\xc4\x99zyk jest zaprojektowany w taki spos\xc3\xb3b, aby mo\xc5\xbcliwa by\xc5\x82a formalna analiza oraz dowodzenie poprawno\xc5\x9bci kodu. Usuni\xc4\x99te zosta\xc5\x82y z niego wszelkie dwuznaczno\xc5\x9bci, elementy sprzyjaj\xc4\x85ce nieprzewidzianym przep\xc5\x82ywom danych (np. wyj\xc4\x85tki), wprowadzono mechanizm formalnych komentarzy (formal comments, annotations). W celu umo\xc5\xbcliwienia silnej weryfikacji poprawno\xc5\x9bci kodu wprowadzono precyzyjne specyfikacje wej\xc5\x9bcia i wyj\xc5\x9bcia poszczeg\xc3\xb3lnych procedur. Ochron\xc4\x99 stabilno\xc5\x9bci zapewnia m.in. wewn\xc4\x99trzna kontrola liczby iteracji oraz czasu wykonania procedur. J\xc4\x99zyk posiada szereg rozszerze\xc5\x84 przeznaczonych do obs\xc5\x82ugi urz\xc4\x85dze\xc5\x84 fizycznych dzia\xc5\x82aj\xc4\x85cych w czasie rzeczywistym np. sensor\xc3\xb3w._NEWLINE_Programy napisane w j\xc4\x99zyku SPARK Ada s\xc4\x85 kompatybilne ze standardowym j\xc4\x99zykiem Ada. Funkcje formalnej analizy poprawno\xc5\x9bci s\xc4\x85 relizowane przez dodatkowe narz\xc4\x99dzia (SPARK Examiner) bazuj\xc4\x85ce g\xc5\x82\xc3\xb3wnie na rozszerzeniach jakimi s\xc4\x85 formalne komentarze. Przyk\xc5\x82ad fragmentu kodu z formalnymi komentarzami SPARK:_NEWLINE_procedure Increment (X : in out Counter_Type);_NEWLINE_--# derives X from X;--# pre X < Counter_Type'Last;--# post X = X~ + 1;_NEWLINE_Komentarze te precyzyjnie okre\xc5\x9blaj\xc4\x85 do jakich zmiennych globalnych odwo\xc5\x82uje si\xc4\x99 dana funkcja oraz w jaki spos\xc3\xb3b wp\xc5\x82ywa ona na warto\xc5\x9b\xc4\x87 zmiennej X (mo\xc5\xbce by\xc4\x87 tylko wi\xc4\x99ksza o 1, nie mniejsza, ani nie r\xc3\xb3wna pocz\xc4\x85tkowej warto\xc5\x9bci) oraz jaka musi by\xc4\x87 pocz\xc4\x85tkowa warto\xc5\x9b\xc4\x87 zmiennej X (mniejsza od najwi\xc4\x99kszej dopuszczalnej warto\xc5\x9bci Counter_Type). Deklaracje te stanowi\xc4\x85 podstaw\xc4\x99 dla formalnej weryfikacji kodu funkcji przez SPARK Examiner, kt\xc3\xb3ry sprawdza czy wynik dzia\xc5\x82ania tego kodu b\xc4\x99dzie zgodny z deklaracjami formalnymi."