Naredna: Prevođenje u C program Gore: NZD Prethodna: Dokaz parcijalne korektnosti programa   Sadržaj


Dokaz zaustavljanja programa

Da bi bila dokazana totalna korektnost programa potrebno je još dokazati da se program za proizvoljan ulaz zaustavlja.

Program se zaista zaustavlja. Naime, nenegativna vrednost promenljive q se u svakoj iteraciji smanjuje i u jednom trenutku (nakon konačno mnogo koraka) mora da dostigne nulu što će izazvati zaustavljanje petlje.

Time smo dokazali da je program totalno korektan, tj. za sve vrednosti ulaznih promenljivih koje zadovoljavaju dati preduslov, program će se zaustaviti i biće ispunjen dati pauslov.




Naredna: Prevođenje u C program Gore: NZD Prethodna: Dokaz parcijalne korektnosti programa   Sadržaj