Niezmiennik pętli

Witam
Mam taką pętlę :

 int k=1, p=n; 
 while (p>0) { 
 k=k+k;
 p=p-1; 
} 
 

Wynikiem jest k i jest to 2^n

Jaki zastosować niezmiennik pętli, który pomoże udowodnić poprawność tego programu ?

Ja bym sobie odwrócił to liczenie 'p' i leciał pętlą od 0 do n. Niezmiennikiem będzie to że k == 2^p w każdym obiegu. U ciebie k == 2^n-p

A niezmiennik takiej pętli :

int k = 1, p =n;
while(p > 0) {
  k = k*p;
  p = p-1;
}
return k;

Kombinowałem analogicznie do poprzedniego przykładu zrobić : k == (n-p) !, no ale to niestety nie jest prawdą. Jest jakaś dobra metoda do znalezienia niezmiennika programu, czy po prostu trzeba kombinować ?

No jak dla mnie to za każdym obiegiem pętli
k = n!/p!

Faktycznie :) Masz jakiś sposób na szukanie tych niezmienników ?

Tak. Proponuje używać do tego mózgu. Patrzysz na pętlę i wymyślasz sobie warunek który jest spełniony w każdym jej obiegu. Gdyby dało sie to robić "automatycznie" to juz dawno mielibyśmy narzędzia do automatycznego dowodzenia poprawności programów, a póki co mamy takie cuda tylko dla bardzo prostych przypadków i tylko dla niektórych języków (typu Ocaml) ;]

Wg mnie: (p-1)!/(n-1)!
Nie wiem co mi strzeliło do łba.
Już wiem co: mi się wydawało że p jest zwiększane.