Niezmiennik pętli

Niezmiennik pętli – pojęcie używane w projektowaniu, analizie i dowodzeniu poprawności algorytmów.

Mówimy, że zdanie P jest niezmiennikiem pętli, jeżeli po każdym jej przebiegu jest ono prawdziwe.

W praktyce niezmiennik pętli traktowany jest jako założenie indukcyjne, na podstawie którego wykazuje się prawdziwość kroku indukcyjnego.

Przykłady

int a=5, b=0;

for (int i=0; i<9; i++) {
    b++;
}

Zdanie a jest równe 5 jest trywialnym niezmiennikiem pętli.

Algorytm Euklidesa wyznaczania największego wspólnego dzielnika (NWD) liczb naturalnych a i b (% jest operatorem modulo, tzn. zwraca resztę z dzielenia):

int NWD(int a, int b) {
    int c;

    while (b != 0) {
        c = a%b;
        a = b;
        b = c;
    }

    return a;
}

Niezmiennikiem pętli pozwalającym dowieść poprawności algorytmu NWD jest zdanie: NWD(a, b)=NWD(b, a mod b).

W sortowaniu przez scalanie zdanie: w i-tym przebiegu pętli Mergesort serie długości i są wewnętrznie posortowane.

Zobacz też

Asercja (informatyka)