Niezmiennik pętli
Z Wikipedii
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.
[edytuj] 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.
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ść 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ętrzenie posortowane.
