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)