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 ?
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 == 2p w każdym obiegu. U ciebie k == 2n-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.