Spis treści
W przypadku niektórych aplikacji (szczególnie krytycznych pod kątem bezpieczeństwa ogólnie pojmowanego) podstawową sprawą jest poprawność programu, która musi być zbadana i ustalona pewnymi rygorystycznymi procedurami formalnymi. W przypadku systemów safety-critical konsekwencją błędu może być utrata życia lub zniszczenie środowiska. W przypadku systemów security-critical zaś, błąd może być równoznaczny z utratą bezpieczeństwa państwa, reputacji w biznesie lub też może umożliwić kradzież.
Aplikacje są pogrupowane na różnych poziomach, w zależności od ryzyka. Dla aplikacji związanych z lotnictwem standard DO-178B [1] definiuje poniższe poziomy:
- Poziom E - brak ryzyka: nie ma problemu; nawalił system rozrywkowy? można skorzystać!
- Poziom D - mały problem: pewne niedogodności; padł system automatycznych toalet.
- Poziom C - poważniejszy problem: jakieś urazy; gwałtowne lądowanie, rany i potłuczenia.
- Poziom B - niebezpiecznie: kilka zgonów; fatalne lądowania i pożar.
- Poziom A - katastrofa: samolot zniszczony, wszyscy nie żyją; uszkodzenie systemu sterowania.
Tak na marginesie: mimo, iż awaria systemu rozrywki została sklasyfikowana na poziomie E, jeśli pilot z powodu usterki tego systemu nie będzie w stanie go wyłączyć (aby - na przykład - oznajmić coś niemiłego), to problem ten należy uznać do klasy problemów z poziomu D.
W przypadku większości programów wymagających certyfikacji przez odpowiedni organ, nie jest wystarczającym, że program jest poprawny. Program musi wykazać, że jest prawidłowy. A to już jest bardziej skomplikowane.
Rozdział ten to bardzo krótkie wprowadzenie do języka Spark. Język stanowi podzbiór języka Ada. Został stworzony z myślą o pisaniu systemów wysokiej integralności. Mimo, iż technicznie rzecz biorąc, jest to podzbiór Ady z dodatkowymi informacjami wstawianymi przy pomocy komentarzy adowych, warto traktować Spark jako odrębny język z własnymi prawami, który dla wygody korzysta z kompilatora Ady, ale który podlega bardziej formalnemu podejściu niż pełny język Ada. Analiza programów napisanych w języku Spark przeprowadzana jest przy pomocy zestawu narzędzi, z których najbardziej ważnymi są: Examiner, Simplifier i Proof Checker.
Rozpoczniemy rozważaniami nad ważnymi kwestiami dotyczącymi poprawności i kontraktów.
11.1 Kontrakty
Co można rozumieć pod pojęciem "poprawne oprogramowanie"? Ogólnie można by rzec: poprawny program to taki, który robi to, co użytkownik miał na myśli. Zwrot "co miał na myśli" może mieć znaczenie dosłownie w przypadku prostego, jednorazowego programu do doraźnych obliczeń. W przypadku dużych systemów stosowanych w lotnictwie może być treścią pewnych pisemnych umów pomiędzy końcowym użytkownikiem a projektantem oprogramowania.
Idea kontraktów programistycznych nie jest nowa. Jeśli wejrzymy w biblioteki programistyczne powstałe we wczesnych latach sześćdziesiątych ubiegłego wieku, szczególnie stosowanych w zagadnieniach matematycznych, być może napisanych w Algolu 60 (język faworyzowany w publikacjach materiałów czasopism Communications of the ACM i Computer Journal), znajdziemy informacje, mówiące jakie parametry są wymagane, jakie ograniczenia zakresów wartości ich dotyczą etc. Informacje te stanowią pewnego rodzaju kontrakt pomiędzy autorem podprogramu a użytkownikiem tegoż. Użytkownik obiecuje przekazywać odpowiednie parametry, a podprogram zapewnia wygenerowanie prawidłowego wyniku.
Dekompozycja programu na różne części składowe jest bardzo znana. Istotą procesu programowania jest zdefiniowanie, co te części robią, a tym samym jakie związki zachodzą pomiędzy nimi. To pozwala na niezależne projektowanie poszczególnych składowych. Jeśli napiszemy każdą część prawidłowo (tak, że spełnia ona swoje zadania wynikające z kontraktu określonego interfejsem), a jednocześnie mam prawidłowo zdefiniowany interfejs, to jesteśmy pewni, że jeśli połączymy te części w jeden kompletny system, wszystko będzie działało jak należy.
Gorzkie doświadczenia pokazują, że życie nie jest tak różowe. Dwie rzeczy nie wychodzą: z jednej strony, definicje interfejsów zazwyczaj nie są kompletne (są luki w kontraktach). Z drugiej zaś strony, poszczególne składowe są niepoprawne lub są niewłaściwie wykorzystywane (kontrakt został naruszony). No i oczywiście, kontrakty mogą mówić nie to, co chcieliśmy wyrazić.
11.2 Poprawność przez budowanie
Spark zachęca do pisania programów w uporządkowany sposób, mający na celu poprawność programu przy pomocy różnych technik wykorzystanych w trakcie budowania. To podejście typu "poprawność przez budowanie" jest w opozycji do innych, których celem jest wygenerowanie jak najwięcej kodu w jak najkrótszym czasie celem poszczycenia się.
Na przestrzeni lat, w czasie których wykorzystano język Spark w budowaniu systemów dla lotnictwa, bankowości i kierowania koleją, nagromadziło się wiele mocnych dowodów na to, że nie tylko programy stały się bardziej poprawne, lecz również, że całkowity koszt budowania systemów jest faktycznie niższy niż koszt całego etapu testowania i integracji razem wziętych.
Przypatrzymy się teraz dokładniej obydwu problemom wspomnianym wyżej. Wpierw, podając kompletną definicję interfejsu, później - upewniając się, że kod prawidłowo implementuje interfejs.
Najlepiej byłoby, gdyby definicja interfejsu pomiędzy składnikami oprogramowania ukrywała wszystkie nieistotne szczegóły, jednocześnie eksponując szczegóły istotne. Inaczej mówiąc, definicja interfejsu powinna być kompletna i poprawna.
Jako prosty przykład definicji interfejsu rozważmy interfejs do podprogramu. Jak już wspomnieliśmy, interfejs winien opisywać pełny kontrakt pomiędzy użytkownikiem a implementatorem. Szczegóły implementacji podprogramu nie powinny nas w tym momencie interesować. Aby móc jasno odróżnić te dwie interesujące nas sprawy, winniśmy skorzystać z języka programowania, w którym są one wyraźnie oddzielone. Niektóre języki przedstawiają podporgramy (funkcje i metody) w jednym kawałku, z interfejsem fizycznie znajdującym się w tym samym miejscu co implementacja. Jest to uciążliwe: nie tylko czyni kontrolę kodu mniej prostą, ponieważ kompilator żąda całego kodu, lecz również zmusza programistę do zmieniania kodu w tym samym czasie, w którym zmienia interfejs, co plącze cały logiczny proces projektowania.
Ada ma strukturę oddzielającą interfejs (specyfikację) od implementacji (treść). Dotyczy to zarówno pojedyncznych podprogramów, jak i grup bytów enkapsulowanych w jednym pakiecie. I to jest zasadniczym powodem, dlaczego Ada tworzy takie dobre podstawy dla języka Spark.
Spark wymaga dodatkowych informacji. Są mu one dostarczane w postaci mechanizmu adnotacji, który wykorzystuje do tego celu komentarze Ady. Zasadniczym przeznaczeniem adnotacji jest zwiększenie liczby informacji na temat interfejsu, bez konieczności dostarczania informacji o implementacji. W rzeczywistości Spark pozwala na dodawanie informacji na różnych poziomach szczegółowości, w zależności od wymagań aplikacji.
Zastanówmy się, jakie informacje są podane przez następującą specyfikację Ady:
procedure Add(X: in Integer);
Szczerze mówiąc, nie za wiele tych informacji. Stwierdzić można tylko, że jest procedura nazwana Add, pobierająca jeden parametr typu Integer, którego formalna nazwa to X. Wystarczy dla kompilatora, który ma za zadanie wygenerować kod wywołujący procedurę. Nic jednak nam nie mówi co ta procedura robi. Mogłoby to być cokolwiek. W szczególności, wcale nie musi niczego dodawać, ani korzystać z wartości X. Procedura mogłaby, na przykład, odjąć od siebie jakieś dwie zmienne globalne, a następnie zapisać wynik do pliku. Lecz teraz zastanówmy się, co się stanie, gdy dodamy adnotację najniższego poziomu. Mogłoby to wyglądać tak:
procedure Add(X: in Integer); --# global in out Total;
Adnotacja ta stwierdza, że jedyną zmienną globalną, do której może mieć dostęp procedura Add to zmienna Total. Dodatkowo, podany tryb mówi nam, że musi zostać wykorzystana wartość początkowa (in) i wygenerowana nowa wartość (out). Reguły języka Spark również więcej mówią nam o parametrze X. Chociaż w Adzie parametr nie musi być w ogóle wykorzystany, to w języku Spark jest wymóg, że parametr w trybie in musi być użyty.
Teraz więc wiemy już znacznie więcej. Wiemy, że wywołanie procedury Add wygeneruje nową wartość zmiennej globalnej Total, do czego wykorzystana będzie wartość początkowa tej zmiennej oraz wartość parametru X. Mamy również pewność, że procedura ta nie może zrobić nic więcej. W szczególności nie może wydrukować niczego, ani spowodować żadnych nieokreślonych efektów ubocznych.
Oczywiście, informacja dotycząca interfejsu nie jest kompletne, gdyż nie jest określone wymaganie, że do uzyskania nowej wartości zmiennej Total potrzebna jest operacja dodawania. Celem uzupełnienia specyfikacji możemy dodać opcjonalne adnotacje ułatwiające proces uzyskania dowodu poprawności:
procedure Add(X: in Integer); --# global in out Total; --# post Total = Total~ + X;
Adnotacja post jest zwana warunkiem końcowym (postcondition) i wyraźnie mówi, że końcowa wartość zmiennej Total to wynik dodania jej wartości początkowej (tutaj oznaczonej jako Total~) do wartości X. W tym momencie możemy uznać, że nasza specyfikacja jest kompletna.
Również można podać warunki wstępne (preconditions). Zakładając, że wartość parametru X musi być zawsze dodatnia, piszemy:
--# pre X > 0;
Ważnym aspektem adnotacji jest to, że wszystkie one są sprawdzane statycznie (przy pomocy narzędzia Examiner oraz innych z pakietu Spark), a nie w trakcie wykonywania programu.
Szczególnie należy podkreślić to, że warunki wstępne i końcowe są sprawdzane przed wykonaniem programu. Jeśli byłyby one sprawdzane w czasie działania programu, to sprawiałoby wrażenie ryglowania drzwi po ucieczce konia (w oryginale gra słów: "it would be a bit like bolting the door after the horse has bolted" i stąd komentarz autora, że objawiła się tutaj właśnie gra słów spowodowana przeciążeniem słownictwa w języku angielskim). Przecież nie chcemy być poinformowani dopiero w czasie działania programu, że zostały naruszone warunki. Przypuśćmy, że mamy warunek wstępny dla lądowania samolotu:
procedure Touchdown( ... ); -- lądowanie --# pre Undercarriage_Down; -- podwozie w dół
Byłoby trochę nieprzydatne stwierdzenie, że podwozie nie jest opuszczone w momencie gdy samolot właśnie ląduje. Naprawdę chcemy być pewni tego, że program był przeanalizowany celem pokazania, że sytuacja taka nie wystąpi.
Przemyślenia te ukazują inny problem związany z programowaniem: zapewnienie, że implementacja poprawnie spełnia warunki kontraktu interfejsu. Mamy do czynienia z tak zwanym odpluskwianiem (debugging). Ogólnie rzecz biorąc, mamy cztery sposoby na znalezienie błędu.
- Przy pomocy kompilatora. Zazwyczaj łatwo jest poprawić błędy, gdyż kompilator dokładnie mówi co jest nieprawidłowe.
- W czasie działania programu przez kontrole wbudowane w język. Dotyczy to języków, które sprawdzają, czy - na przykład - nie będziemy zapisywać danych poza obszarem tablicy. Zazwyczaj otrzymamy w takiej sytuacji komunikat błędu, mówiący jaka struktura została naruszona i w którym miejscu programu to nastąpiło.
- Poprzez testowanie. Oznacza to uruchamianie różnych przykładów, ślęczenie nad (nie)oczekiwanymi błędami i zastanawianie się, gdzie coś poszło nie tak.
- Przez załamanie systemu. Często ulega zniszczeniu wiele wskazówek, a także może być bardzo nudne.
Owe cztery sposoby obrazują wzrost trudności. Błędy łatwiej znaleźć i poprawić na jak najwcześniejszym etapie. Dobre narzędzia programistyczne to te, które przemieszczają błędy z jednej kategorii do drugiej, tej o niższym numerze. A zatem, dobre języki programowania to takie, które dostarczają mechanizmów chroniących przed błędami trudnymi do znalezienia. Ada jest szczególnie dobrym językiem, a to dlatego, że posiada ścisłą typizację oraz kontrole w czasie działania programu. Na przykład, prawidłowe wykorzystanie pojęcia typów wyliczeniowych zmienia trudne błędy typu trzeciego na błędy typu pierwszego, czyli łatwe do wykrycia (patrz: Bezpieczny system typów).
Głównym zadaniem języka Spark jest umocnienie definichi interfejsów (kontraktów) poprzez przesuwanie wszystkich błędów do niższych kategorii, najlepiej do typu pierwszego, gdzie błędy są odnajdywane przed uruchomieniem programu. Uzyskujemy to dzięki globalnym adnotacjom, dzięki które uniemożliwiają przypadkową zmianę niewłaściwych zmiennych globalnych. Podobnie wykrywanie naruszeń warunków wstępnych i końcowych przemieszcza błędy do kategorii pierwszej. Jednak stwierdzenie, że naruszenia takie na pewno nie wystąpią potrzebne jest przeprowadzenie dowodu matematycznego. Nie zawsze jest to proste, ale mamy do dyspozycji narzędzia z pakietu Spark, które w znacznym stopniu automatyzują ten proces.
11.3 Język rdzenia
Ada jest barfzo bogatym językiem, dlatego niektóre jej możliwości czynią proces całkowitej analizy programu bardzo skomplikowanym. Z tego powodu podzbiór w postaci języka Spark pomija pewne mechanizmy. W większości są to mechanizmy mające charakter dynamiczny Na przykład, brak jest typów dostępowych, brak dynamicznego wywoływania dyspozycyjnego, wyjątków. Cała wykorzystywana pamięć ma charakter statyczny, stąd, tablice muszą mieć granice statyczne (ale parametry do podprogramów mogą być dynamiczne). No i brak jest rekursji.
Mechanizmy zadaniowości wykazują szczególne tendencje dynamiczne i z tego powodu Spark udostępnia jedynie profil Ravenscar (Bezpieczna wielozadaniowość).
Innym ograniczeniem wspomagającym analizę jest to, że każdy byt musi mieć swoją nazwę. I każda taka nazwa powinna jednoznacznie określać tylko jeden byt. Stąd wymóg nazywania wszystkich typów i podtypów z jednoczesnym uniemożliwieniem przeciążania. Z drugiej strony tradycyjne struktury blokowe są dozwolone - nie ma ograniczeń na stosowanie nazw lokalnych. Co więcej, dozwolone jest używanie typów znakowanych, przy jednoczesnej blokadzie korzystania z typów klasowych.
Idea stanu jest pierwszoplanowa dla procesu analizy. Stąd mocne rozróżnienie pomiędzy procedurami, zmieniającymi stan, a funkcjami, które ten stan obserwują (patrz odróżnianie instrukcji i wyrażeń w rozdziale Bezpieczna składnia). W języku Spark funkcje nie mogą dawać absolutnie żadnych skutków ubocznych.
Otrzymany rdzeń okazuje się być wystarczająco ekspresyjny, by spełnić wymagania krytycznych aplikacji, które nie chcą korzystać z określonych cech takich jak dynamiczna obsługa pamięci.
11.4 Zestaw narzędzi
W pakiecie Spark mamy do dyspozycji trzy podstawowe narzędzia: Examiner, Simplifier i Proof Checker.
Examiner to narzędzie najważniejsze. Spełnia dwie podstawowe funkcje:
- Sprawdza zgodność kodu z regułami języka.
- Sprawdza spójność pomiędzy kodem a wprowadzonymi adnotacjami przy pomocy analizy przepływu.
Kontrole te Examiner w dużej mierze przeprowadza analizując interfejsy pomiędzy składowymi, celem stwierdzenia że obie strony rzeczywiście spełniają wymagania interfejsów. Interfejsy to oczywiście specyfikacje pakietów i podprogramów, a adnotacje wzbogacają informacje o tych interfejsach, a tym samym poprawiają jakość kontraktów pomiędzy implementacją składowych a użytkownikami tych składowych.
Nawiasem mówiąc, sam Examiner jest napisany w języku Spark i został zastosowany w procesie swego powstawania, dlatego możemy mieć duże zaufanie do wyników pracy tego narzędzia.
Adnotacje rdzenia zapewniają nas, że program będzie wolny od błędów związanych z przepływem informacji. Tak, więc Examiner wykrywa wykrywa użycie niezainicjowanych zmiennych i nadpisuje wartości przed ich użyciem. Dlatego tak ważnym jest, by nie nadawać zmiennym nieużytecznych wartości tylko dla zasady (patrz rozdział Bezpieczny start programu), ponieważ utrudni to wykrywanie błędów przepływu informacji.
Jednak do badania zachowania dynamicznego adnotacje rdzenia nie są przeznaczone. W tym celu możemy wstawić kilka adnotacji dowodzeniowych (takich jak warunki wstępne i końcowe), pozwalających na analizę takiego zachowania przed wykonaniem programu. Adnotacje dowodzeniowe umożliwiają narzędziu Examiner wygenerowanie zbiór domniemań (potencjalnych twierdzeń), które muszą być udowodnione, celem stwierdzenia, że program jest prawidłowy w odniesieniu do adnotacji. Adnotacje dowodzeniowe dotyczą:
- warunków wstępnych i końcowych podprogramów,
