Nie zawsze da się algorytmicznie sprawdzić, czy dwa programy robią dokładnie to samo
Dla dowolnych programów o pełnej mocy obliczeniowej problem równoważności — czy oba zachowują się tak samo dla wszystkich możliwych wejść — jest nierozstrzygalny. Nie istnieje więc uniwersalny program, który bierze dwie dowolne implementacje, zawsze kończy i bezbłędnie odpowiada „tak” lub „nie” na pytanie o ich pełną równoważność. Dowód można uzyskać przez redukcję z problemu stopu. To nie oznacza, że kompilatory nie mogą udowadniać poprawności optymalizacji ani że testy są bezużyteczne. Oznacza, że w pełnej ogólności trzeba korzystać z ograniczonych klas programów, formalnych dowodów dla konkretnych przypadków lub metod, które czasem nie potrafią rozstrzygnąć.
Równe wyniki na kilku testach to za mało
Dwa programy mogą zgadzać się dla miliona testów i różnić dopiero na jednym bardzo szczególnym wejściu. Pełna równoważność wymaga stwierdzenia zgodności dla wszystkich wejść, a przy programach, które mogą się nie kończyć, trzeba dodatkowo uwzględnić zachowanie związane z terminacją. Skończony zestaw zwykłych testów nie daje sam z siebie takiej gwarancji dla nieskończonej przestrzeni przypadków.
Redukcja z problemu stopu
Materiały z teorii obliczeń pokazują standardową konstrukcję: gdyby istniał decydent równoważności programów, można byłoby przekształcić pytanie o zatrzymanie programu w pytanie, czy dwa specjalnie skonstruowane programy są równoważne. Otrzymalibyśmy wtedy decydent problemu stopu, którego istnienie jest niemożliwe. Wniosek: uniwersalna równoważność programów również jest nierozstrzygalna.
A jednak kompilatory optymalizują kod
Optymalizator kompilatora często zastępuje fragment programu innym fragmentem i musi mieć podstawę, by uznać transformację za bezpieczną. Nie rozwiązuje przy tym ogólnego problemu równoważności dwóch dowolnych programów. Stosuje reguły o udowodnionej poprawności w określonym kontekście, analizuje ograniczoną reprezentację pośrednią albo korzysta z lokalnych własności. To znacznie węższe zadanie niż pełna równoważność wszystkiego ze wszystkim.
Formalna weryfikacja zmienia rodzaj pracy
Dla konkretnej pary programów można czasem dostarczyć dowód równoważności w logice lub systemie weryfikacji. Nierozstrzygalność nie mówi, że żaden taki dowód nie istnieje; mówi, że nie ma ogólnej, zawsze kończącej procedury automatycznie rozstrzygającej wszystkie przypadki. Człowiek, dodatkowe niezmienniki i specjalna teoria domeny mogą umożliwić sukces tam, gdzie uniwersalny decydent nie może istnieć.
Granica między testowaniem i dowodzeniem
Testy są doskonałe do znajdowania różnic, jeśli trafią na kontrprzykład. Wykazanie pełnej równoważności jest mocniejszym wymaganiem. Ta różnica tłumaczy, dlaczego w krytycznych systemach łączy się testowanie, statyczną analizę, typy, kontrakty i dowody formalne: żadne pojedyncze uniwersalne narzędzie nie może mechanicznie rozstrzygnąć wszystkich semantycznych pytań o dowolny program.
Ograniczenie języka może przywrócić rozstrzygalność
Nierozstrzygalność równoważności dotyczy wystarczająco ogólnego modelu programów, zdolnego do uniwersalnych obliczeń. Inżynieria często omija tę barierę przez pracę w ograniczonej klasie: narzędzie może analizować programy bez nieograniczonych pętli, obwody o ustalonej strukturze, ograniczony język zapytań albo tylko skończony zakres wejść. Wtedy pytanie, które w pełnej ogólności nie ma algorytmu, może stać się rozstrzygalne. To ważny wzorzec projektowy: zamiast żądać magicznego testera „dla każdego programu”, definiuje się domenę na tyle precyzyjnie, aby automatyczna weryfikacja miała matematyczne podstawy.
Testy pozostają potrzebne mimo matematycznej bariery
Nierozstrzygalność nie odbiera sensu testom jednostkowym, fuzzingowi ani dowodom formalnym. Każda z tych metod ma inny zakres: test obejmuje wybrane wykonania, fuzzing intensywnie próbuje wiele przypadków, a formalny dowód może działać dla programu i specyfikacji, które mieszczą się w możliwościach danego systemu. Granica mówi tylko, że nie istnieje jeden zawsze kończący się algorytm, który bez dodatkowych ograniczeń rozstrzyga równoważność dowolnej pary programów.