niektóre z odmian rachunku lambda takie jak System F.
Podejście formalne Niech oznacza wektor danych wejściowych algorytmu niech będzie wektorem wynikowym Przebieg algorytmu dla dowolnych (w granicy zakładanej poprawności) danych jest jednoznacznie wyznaczony przez ciąg przekształceń:
gdzie są danymi przejściowymi.
W praktyce należy wykazać, że ciąg przekształceń jest zawsze skończony, oraz wektor zawiera poprawne dane. Najczęściej stosowaną techniką jest indukcja matematyczna, z zastosowaniem niezmienników pętli.
Przykład Poprawności algorytmu Euklidesa można dowieść, pokazując, że zdanie:
jest niezmiennikiem pętli algorytmu NWD.
Ponieważ wartość drugiego argumentu spada po każdej iteracji, więc algorytm zawsze zakończy działanie.
Z niezmiennika pętli wynika:
A więc, po ostatnim przebiegu pętli algorytm zwróci wartość
Zobacz też automatyczne dowodzenie twierdzeń dowód niezmiennik pętli problem stopu
Kategoria:Teoria obliczeń