Widzę w buzzie długą, fachową dyskysję o sprawdzaniu poprawności programów. Niestety, nie jestem w stanie jej rozumieć. Mam za duże dziury erudycyjne w zakresie wiedzy o różnych programach, narzędziach, ... - nie jestem informatykiem. Temat jednak mnie ciekawi. Programy, nawet krótkie, potrafią być naprawdę trudne, mogą się opierać na bardzo nieoczywistych algorytmach, opierających się na wysoce nietrywialnych twierdzeniach. Czyż program sprawdzający poprawność programów, ale tak na pewniaka, nie musiałby mieć ogromnej wiedzy? Przerastającej wiedzę schowaną w programach?
Dla łatwego wprowadzenia tematu chcę zacząć od czegoś bardzo prostego, od zmyślonej sytuacji:
Pewien fizyk potrzebuje pliku z parami (punkt prosta), gdzie chodzi o pary incydentne, brane z płaszczyzny afinicznej rzędu 9 (ma 81 punktów), standardowej, nad ciałem GF(9). Zatrudnił więc fizyk programistę, żeby mu ten plik sprokurował. Poza tym od programisty wziął program, który programista napisał, żeby wygenerować żądaną płaszczyznę.
A teraz fizyk ma wątpliwości co do poprawności pliku i programu. Jak program sprawdzający poprawność pomoże fizykowi? Powiedzmy, że złośliwy programista poprawnie zaprogramował, ale niestandardową płaszczyznę. Odróżnić ją od standardowej jest bardzo trudno, ma szereg własności takich samych. Program sprawdzający poprawność mógłby nawet machnąć ręką (:-) na kod, i sprawdzić poprawność outputu. Porównać go z płaszczyzną standardową. Takie rzeczy robią CAD programy. Ogólnie taki problem, sprawdzający izomorfizm dwóch grafów, jest NP-complete (?), jest niewielomianowy. Więc gdyby chodziło o płaszczyzny wyższego rzędu, to CAD programy wysiadłyby, mimo że można takie płaszczyzny łatwo generować (dostać outputowy plik, przedstawiający graf punktowo-liniowy). Jeżeli programy CAD wysiadłyby, to jak sobie poradzi program sprawdzający poprawność? Musi jednak zajrzeć do kodu - powodzenia! Kod jest poprawny w pewnym sensie, ale produkuje płaszczyznę nieizomorficzną z żądaną. Dowód niepoprawności kodu wydaje mi się znacznie trudniejszym problemem niż dowód niepoprawności outputowego pliku; najprościej byłoby program puścić i analizować jednak output. Ba!
Oczywiście w przypadkach ogólnych sprawdzanie outputu jest niemożliwe, bo w zależności od inputu, output może być ogromny (a zastosowanie może korzystać tylko z małej części outputu, ale a priori z dowolnej, w zależności od losowych parametrów).
Może jednak zacznijmy od malutkiej 81-punktowej płaszczyzny nad ciałem GF(9).
To dosyć zabawne ale przykłąd który podałeś jest bardzo poważnym argumentem za ścisłą weryfikacją kodu a nie przeciw niej. Jeśli masz program który generuje 10^3 liczb z skończonej struktury matematycznej X, która zawiera tych liczb 10^200 to jedyną możliwością sprawdzenia czy programista piszą stosowne funkcje się nie pomylił jest wykazanie że kod programu realizuje faktycznie stosowną funkcje o wartościach wyłącznie w zbiorze X. Badanie statystyczne zbioru wyników dla 3 przypadków ( zamiast 3 możesz wpisać dowolną osiągalną w praktyce liczbę) nic tu nie wykaże.
ReplyDelete