Jak nauczyliśmy maszyny liczyć i myśleć za nas? Część 21: Jak walczyć z błędami programów?

W poprzednim odcinku tego cyklu felietonów przedstawiłem kilka informacji na temat skutków błędów w programach. Wspomniane wyżej przykłady to „wierzchołek góry lodowej” – mała część ogromnej liczby różnych problemów, na które natknęła się coraz bardziej uzależniona od komputerów działalność ludzi i instytucji. Większość tych problemów pojawiła się na skutek występowania błędów w programach.

Błędy w programach komputerowych są bardzo trudne do wykrycia. Gdy już ustalimy, że błąd jest – jego lokalizacja i usunięcie nie stanowią zasadniczego problemu. Ale jak się upewnić, że żadnego błędu nie ma? To jeden z najpoważniejszych problemów informatyki.

Testowanie, czyli walka z błędami

Próbowano różnych metod formalnych, o których napiszę dalej, ale praktyka jest taka, że programy po ich napisaniu się testuje. Polega to na wielokrotnym uruchamianiu programu z różnymi zestawami danych wejściowych, dla których prawidłowy wynik jest znany i może być sprawdzony.

We wczesnym okresie rozwoju informatyki (do 1956 r.) wspomniany wyżej debugging (mający na celu wykrycie ewidentnych błędów popełnionych przez programistę) oraz testowanie programu traktowano jako w istocie tę samą czynność. Było to po prostu empiryczne badanie przydatności do użycia stworzonego programu. W 1957 r. Charles L. Baker (RAND Corporation) wprowadził rozróżnienie pomiędzy debuggingiem, czyli szukaniem błędów, a testowaniem badającym wszechstronnie właściwości (zalety i wady) programów.

Debugging jest czynnością stosowaną zawsze w odniesieniu do nowych programów, ale jest to działanie bardzo pracochłonne i frustrujące. Sam autor programu nie jest w stanie przeprowadzić kompletnych i wyczerpujących testów swojego programu, ponieważ błędy zwykle ujawniają się w takich okolicznościach, których autor nie mógł sobie wyobrazić, pisząc program, a zatem nie wymyśli ich także podczas testów.

Pamiętajmy: własnego błędu z reguły się nie widzi!

Zawodowi testerzy

Człowiekiem, który jako pierwszy zorganizował specjalny zespół testerów, był Gerald M. Weinberg w 1958 r. Weinberg miał powody, żeby troszczyć się o wysoką jakość pisanych programów powstających w jego zespole, ponieważ zespół ten tworzył oprogramowanie dla projektu Merkury – pierwszych amerykańskich lotów załogowych w Kosmos. Było oczywiste, że każdy błąd w programie może kosztować życie astronauty i oznaczać kompromitację na oczach całego świata. Dzięki uporowi Weinberga oprogramowanie misji Merkury zadziałało bez zarzutu i 5 maja 1961 r. pierwszy Amerykanin (Alan Shepard) poleciał bezpiecznie w Kosmos.

Testowanie oprogramowania stało się obowiązującą procedurą w przypadku większości dużych projektów informatycznych – i ten stan trwa do dzisiaj. Natomiast w dobrych firmach produkujących oprogramowanie są całe zespoły dociekliwych, a nawet zawodowo złośliwych testerów, którzy sprawdzają program w każdych okolicznościach. Programiści nazywają czasem owych testerów „zawodowymi idiotami”, ponieważ podczas testów starają się oni sprawdzić, jak się zachowa program, gdy osoba korzystająca z niego będzie wydawać nawet najbardziej idiotyczne polecenia. Oczywiście na głupie pytanie komputer nie dostarczy mądrej odpowiedzi, bo to niemożliwe, ale musi się zachować jak bokser po mocnym ciosie – może się zachwiać, ale nie może paść! Metodologiczne podstawy tego działania zdefiniował w 1975 r. Tom Gilb, który w pracy „Laws of Unreliability” precyzyjnie opisał relacje między błędem ludzkim a błędem systemu.

Duże firmy dbające o swoją renomę zatrudniają wielu testerów i nękają produkowane programy w najróżniejszy sposób – bo od tego zależy ich renoma. Programista tworzący program na doraźne potrzeby z reguły nie ma sił i środków, żeby go dokładnie zbadać. Jest to jeden z ważnych argumentów przemawiających za tym, aby mając problem do rozwiązania, nie starać się go rozwiązać za pomocą własnego programu, tylko szukać dobrego programu firmowego – nawet jeśli za jego użycie trzeba będzie zapłacić.

Na początku XXI w. zawód testera oprogramowania został na stałe wpisany na listę zawodów związanych z informatyką, pojawiły się pierwsze czasopisma zajmujące się tylko tą problematyką, powstały liczne stowarzyszenia i instytucje wspierające aktywność zawodową testerów, organizowane są konferencje naukowe poświęcone testowaniu.

Nie można jednak zapominać o tym, że jeszcze w 1976 r. jeden z pionierów informatyki, Edsger W. Dijkstra, sformułował jedną z najważniejszych zasad testowania: „Testowanie ujawnia obecność defektów, a nie ich brak”. Innymi słowy, jeśli test wykazał, że program zawiera jakieś „pluskwy”, to one naprawdę tam są (i trzeba je oczywiście usunąć). Ale jeśli test przebiegł pomyślnie i niczego nie wykrył, to wcale nie musi oznaczać, że w programie nie ma błędów. Mogą być – tylko nie zostały wykryte!

Próba podejścia teoretycznego

Fakt, że testowanie oprogramowania nigdy nie dawało pewności, że program nie zawiera błędów, doprowadził do tego, że do rozwiązania tego problemu starano się zaangażować wyrafinowaną teorię. Próbowano mianowicie stworzyć metody, które by pozwalały matematycznie dowodzić poprawności programów w taki sam sposób, jak dowodzi się prawdziwości twierdzeń matematycznych. Ponieważ równocześnie w ramach sztucznej inteligencji rozwinięto metody automatycznego dowodzenia twierdzeń, wydawało się, że sam komputer może sprawdzić poprawność napisanego przez człowieka programu. Miał przy tym skorzystać z podejścia, jakie po raz pierwszy zastosowali Allen Newell i Herbert Simon w 1956 r. przy budowie programu Logic Theorist, który był jednym z kroków milowych w badaniach nad sztuczną inteligencją. Dowodził on bardzo sprawnie twierdzeń w obszarze logiki matematycznej, a wsławił się tym, że udowodnił wszystkie twierdzenia z pomnikowego dzieła Bertranda Russella zatytułowanego „Principia mathematica”. Nie dość, że program sam przeprowadził wymagane dowody, to w kilku przypadkach znalazł dowody lepsze niż te podane przez Russella, co ogromnie wsławiło jego twórców.

W udoskonalonych wersjach tej metody automatycznego dowodzenia twierdzeń zasadniczą rolę odgrywała zasada rezolucji sformułowana przez Alana Robinsona w 1965 r. Tak więc narzędzia do komputerowego wspomagania dowodzenia twierdzeń matematycznych istniały już pod koniec lat 60. XX wieku, z czego – po okresie początkowego niedowierzania – zaczęli coraz śmielej korzystać matematycy. Jednak nadzieja, że metody te znajdą zastosowanie jako metoda dowodzenia poprawności programów, okazała się złudna.

Wyjaśnijmy może, jak zamienić program w twierdzenie, które można (ewentualnie) udowodnić. Zacząć trzeba od tego, że specyfikację danych wejściowych i cały tekst badanego programu trzeba potraktować jako założenia twierdzenia matematycznego, a specyfikację wszystkich własności zbioru wyników, które produkuje program, uczynić dowodzoną tezą tego twierdzenia. Jeśli uda się przeprowadzić dowód, że z założeń wynika teza, to udowodnimy, że przy dowolnych (byle poprawnych!) danych wejściowych otrzymuje się zawsze poprawne wyniki. To nieporównanie mocniejszy argument wskazujący, że program jest poprawny, niż jakiekolwiek testy, które są w stanie wykazać jedynie to, że dla niektórych danych wejściowych otrzymuje się poprawne wyniki. Przy dowiedzionym twierdzeniu poprawność programu jest gwarantowana dla wszelkich danych.

Podejście oparte na matematycznym dowodzeniu poprawności programów okazało się bardzo trudne. Podobno jedynym dużym programem, którego poprawność udało się udowodnić matematycznie w opisany wyżej sposób, był program sterujący funkcjonowaniem paryskiego metra. Ale tę informację zaczerpnąłem ze źródeł mówionych (referatów na konferencjach międzynarodowych poświęconych poprawności i niezawodności programów), a nie źródeł pisanych, dlatego przytaczam ją tu bez gwarancji. Ale faktem jest, że o innych matematycznych dowodach poprawności programów wcale nie słychać...

Czy problem „pluskwy milenijnej” może powrócić?

W poprzednim felietonie opowiedziałem o błędzie informatycznym, który mógł potężnie wstrząsnąć światem z powodu niefortunnego sposobu zapisu dat w systemach informatycznych. Kłopotów było mnóstwo, ale kryzys zażegnano. Z problemu „pluskwy milenijnej” śmiali się użytkownicy systemów operacyjnych Unix oraz wzorowany na nim Linux (o obydwu napiszę w dalszych odcinkach tej serii), ponieważ czas w tych systemach określany jest na podstawie zliczania liczby sekund, jakie upłynęły od umownego momentu „rozpoczęcia epoki Unixa”. Owo rozpoczęcie epoki miało miejsce 1 stycznia 1970 r., dokładnie w momencie 00:00:00. No i tak sobie wszystkie programy w systemach Unix oraz Linux działają, zliczając te sekundy. Ale to się im też „urwie”. Powód jest prosty: owe zliczane sekundy zapisywane są jako 32-bitowe liczby całkowite. Na pozór takich liczb można zapisać bardzo dużo, konkretnie 2 147 483 647. Ponad 2 miliardy! Ale wszystko ma swój kres... i zapisywanie biegnących sekund skończy się 19 stycznia 2038 r. o godz. 03:14:07 UTC. Następna sekunda spowoduje przepełnienie licznika i ustawienie daty na... 13 grudnia 1901 r., godz. 20:4:52 UTC.

Oczywiście już trwają prace, które mają zapobiec temu kryzysowi, ale widać, że w informatyce naprawdę czai się mnóstwo pułapek.

Dobry żart na koniec

Tematyka dzisiejszego felietonu była smutna, bo problem błędów w programach do wesołych nie należy. Na koniec więc pozwolę sobie przytoczyć pewien żart dla poprawy nastroju.

Użytkownicy komputerów, stykając się z błędami w używanych programach, często zwracają się do serwisu firmowego, wierząc, że jest jakiś magiczny sposób na to, by skutki tych błędów usunąć, tylko owe firmy ukrywają ten sposób, żeby czerpać dodatkowe korzyści finansowe albo prestiżowe. Ilustracją takiej sytuacji jest poniższa anegdota.

Użytkownik dzwoni do serwisu: – Używam programu Windows, a mój komputer dymi!

Serwisant cierpliwie tłumaczy, że problem nie jest związany z programem, tylko z elektroniką. Po prostu zepsuł się zasilacz. Ale użytkownik się upiera, że potrzebne jest mu tylko hasło, żeby problem zniknął. Po dłuższej wymianie zdań znękany serwisant mówi: – Powiem panu coś w tajemnicy. Otóż jest takie nigdzie nieopisane polecenie systemu Windows, które stosujemy w takich przypadkach. Trzeba wejść do panelu sterowania i wpisać polecenie: „Don’t smoke!”...

– Wiedziałem, wiedziałem, wiedziałem! – krzyczy podekscytowany użytkownik.

Za chwilę jednak dzwoni ponownie:

– Wpisałem „Don’t smoke!”, a komputer nadal dymi!

– No tak, bo to nowe polecenie, a pana zasilacz jest stary i jest niekompatybilny z naszymi nowymi poleceniami. Musi pan wymienić zasilacz na nowy i polecenie „Don’t smoke!” będzie działało.

– Dobrze, tak zrobię! – mówi uradowany użytkownik.

I wymienia zasilacz...