Za ovaj primer nije teško dokazati i totalnu korektnost programa. Primetimo da y ima pozitivnu vrednost, a da je promenljiva r inicijalno postavljena na x i veća od nule. Kako se r umanjuje za y u svakoj iteraciji a y ostaje nepromenjena, to će vrednost promenljive r u jednom trenutku postati manja od y i to će izazvati zaustavljanje programa čime je dokazana totalna korektnost programa.
Naredna: Prevođenje u C program Gore: Celobrojno deljenje Prethodna: Dokaz parcijalne korektnosti programa Sadržaj