Io-1-wyk-Slajd79
Silnia(2)
No to teraz wystarczy tylko dowieść, że jeżeli na początku wykonania podprogramu n >= 0, to na końcu s będzie równe n!. Łatwo powiedzieć, trudno zrobić. W przypadku naszego programu najtrudniejszym elementem jest pętla while . Dowodzenie poprawności programu zawierających pętle odbywa się metodą niezmienników (ang. invariant ). Niezmiennik jest to zdanie, które jest prawdziwe za każdym razem, kiedy powtarzane jest wykonanie instrukcji zawartych w pętli. Dokładnie mówiąc, niezmiennik powinien być prawdziwy tuż przed pierwszym wykonaniem instrukcji zawartych w pętli, tuż przed drugim wykonaniem, przed trzecim itd. Zasadniczy problem polega na tym by znaleźć (wymyślić) taki niezmiennik, który zawsze będzie prawdziwy i jednocześnie pomoże nam w udowodnieniu warunku końcowego POST.
