Prevedimo sada program iz paskalolikog jezika (za koji smo dokazali totalnu korektnost), u C program vodeći računa da pri tome ne narušimo invarijantu petlje i korektnost programa.
Da bi program imao smisla, moramo obezbediti unošenje vrednosti ulaznih promenljivih x i y od strane korisnika, kao i ispis rezultata na standardni izlaz. Potrebno je voditi računa i o deklaraciji i tipu promenljivih. Kako promenljive x i y mogu imati samo celobrojne nenegativne vrednosti, njihov tip će biti neoznačen ceo broj, pritom potrebno je proveriti da li su ulazne vrednosti jednake nuli. Takođe, podrazumevamo da je podržana operacija % koja izračunava ostatak pri celobrojnom deljenju. Time dobijamo sledeći program:
#include<stdio.h> #include<stdlib.h> main() { unsigned int x, y, z; unsigned int p, q, pom; printf("Unesite prirodne brojeve x i y za koje zelite da izracunate NZD:\n"); scanf("%d%d", &x, &y); if ((x == 0) || (y == 0)) { printf("Greska pri unosu vrednosti!\n"); exit(1); } p = x; q = y; if (p<q) { pom = p; p = q; q = pom; } while (q != 0) { pom = q; q = p % q; p = pom; } z = p; printf("NZD(%d, %d) = %d\n", x, y, z); }Broj pomoćnih promenljivih prethodnog programa može da se smanji. Takođe, uslov (q != 0) ekvivalentan je uslovu (q). Dakle, prethodni program postaje:
#include<stdio.h> #include<stdlib.h> main() { unsigned int x, y, pom; printf("Unesite prirodne brojeve x i y za koje zelite da izracunate NZD:\n"); scanf("%d%d", &x, &y); if ((x == 0) || (y == 0)) { printf("Greska pri unosu vrednosti!\n"); exit(1); } printf("NZD(%d, %d) = ", x, y); if (x<y) { pom = x; x = y; y = pom; } while (y) { pom = y; y = x % y; x = pom; } printf("%d\n", x); }
Na ovaj način smo došli do kraja razvojnog puta programa za izračunavanje najvećeg zajedničkog delioca prirodnih projeva x i y. Pri tome, znamo da se on uvek zaustavlja i da je korektan za sve vrednosti ulaznih parametara.