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.

Algorytm Euklidesa wyznaczania największego wspólnego dzielnika (NWD) liczb naturalnych a i b:

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.