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.

<< Poprzedni slajd | Spis treści | Następny slajd >>