Io-1-wyk-Slajd93
Z Studia Informatyczne
Silnia(16)
Aby dowieść prawdziwość warunku końcowego (POST) wystarczy zauważyć, że zaraz po wykonaniu instrukcji while prawdziwy jest inwariant „s jest równe k!” oraz prawdziwe jest zaprzeczenie warunku występującego w instrukcji while , czyli k jest równe n.