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.