Metody dowodzenia poprawności cz II 2

Współczesne badania w dziedzinie poprawności algorytmów:

Idą one w kilku kierunkach:

1.    tworzenie jeżyka asercii — jak pisać asercje, by były jednoznaczne i by było łatwo sprawdzać ich prawdziwość (tego właśnie dotyczyły nasze reguły)

2.    analiza przepływu danych — metodologia symbolicznego śledzenia przepływu danych w algorytmie pozwalająca wykryć błędy bez konieczności implementacji maszynowej algorytmu

3.    logiki programów bądź algorytmów — pozwalają badać równoważność algorytmów dla znalezienia prostych, ale równie poprawnych wersji. W odróżnieniu od klasycznych systemów logiki matematycznej mają one charakter dynamiczny, t.j. prawdziwość zdań w tym systemie zależy nie tylko od bieżącego stanu układu, ale i od powiązań z innymi hipotetycznymi stanami

4.    problemy transformacji algorytmów — iak ie przekształcić. bv zachować równoważność

Dawid Harel w swej książce o algorytmice kończy rozważania o badani poprawności algorytmów i opartych na nich programach pewnym problemem natury bardziej ogólnej: czy można sie zgodzić na to. bv absolutna prawda matematyczna — wynik działania algorytmu czy programu zależała od nieweryfikowalnego oprogramowania. Fizycy i inżynierowie godzą się na takie rozwiązanie, ale tu chodzi o matematykę, o możliwość przeprowadzenia absolutnego dowodu matematycznego przy pomocy komputera.

Jako przykład przytacza zagadnienie z typologii: twierdzenie czterech barw. Jest to problem ilu barw trzeba użyć, by pokolorować mapy dowolnej liczby państw, tak by państwa mające wspólną linię graniczną (nie wspólny punkt, to możliwe) nie były pokolorowane tą samą barwą. Problem powstał w 1852 r. i przez ponad 120 lat nikt nie potrafił udowodnić obserwacji empirycznej, że wystarczają 4 barwy. W 1976 r. dwóch matematyków przeanalizowało problem i dotychczasowe próby dowodzenia i pokazało, że ogólny problem można sprowadzić do pokazania, że skończona liczba przypadków o określonych właściwościach da się pokolorować 4 barwami. Potem użyli komputera do przeanalizowania tych specyficznych przypadków (było ich około 1700) i w ten sposób doyyiedli twierdzenia. Dowód ten został zaakceptowany przez społeczność matematyczną, ale nikt nigdy nie zweryfikował poprawności użytych w tym celu algorytmów i programów (bo nie był w stanie). Czy zatem prawdy absolutnej może zależeć od nieweryfikowalnych algorytmów i programów?