Niezmiennik pętli

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacji, wyszukiwania

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[edytuj | edytuj kod]

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 (% oznacza dzielenie 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.