Dokazom da je uslov y=faktorijel(z) invarijanta petlje dokazano je da program zadovoljava uslove specifikacije i time je dokazana parcijalna korektnost programa.
Da bi bila dokazana totalna korektnost programa potrebno je još dokazati da se program za proizvoljan ulaz zaustavlja.
Program se zaista zaustavlja. Naime, pošto je x nenegativna vrednost, a promenljiva z je inicijalno postavljena na nulu i uvećava se za jedan u svakoj iteraciji, vrednost promenljive z će dostići x i to će izazvati zaustavljanje petlje nakon konačno mnogo koraka.
Time smo dokazali da je program totalno korektan, tj. za sve vrednosti ulazne promenljive koje zadovoljavaju dati preduslov, program će se zaustaviti i biće ispunjen dati pauslov.