U cilju dokazivanja totalne korektnosti programa, jednostavno se može dokazati da se program zaustavlja nakon konačno mnogo koraka. Kako se promenljiva z1 inicijalno postavlja na vrednost y, to iz preduslova važi da z1 ima konačnu vrednost veću od 0. Kako se pri svakom prolasku kroz prvu petlju z1 množi sa 2 a vrednost promenljive r se ne menja, to će u jednom trenutku, nakon konačno mnogo koraka, uslov izlaska iz petlje r ≤ z1 biti ispunjen.
Uslov izlaska iz druge petlje će takođe biti ispunjen nakon konačno mnogo koraka. Naime, vrednost promenljive z2, inicijalno postavljene na 1, će su u toku svakog prolaska kroz prvu petlju množiti sa 2. Kako se iz prve petlje izlazi nakon konačno mnogo koraka, to će i vrednost promenljive z2 po izlasku iz petlje biti konačan broj. Pri svakom prolasku kroz drugu petlju, vrednost promenljive z2 se deli sa 2, pa kako je z2 konačan broj, to će nakon konačno mnogo koraka njegova vrednost postati jednaka sa 1, što je ujedno i uslov izlaska iz druge petlje.
Dakle, nakon konačno mnogo koraka, program se završava, čime je dokazana totalna korektnost programa.
Naredna: Prevođenje u C program Gore: Celobrojni koren Prethodna: Dokaz parcijalne korektnosti programa Sadržaj