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 moramo voditi računa da y mora biti različito od nule. Takođe, podrazumevamo da su podržane operacije oduzimanja i sabiranja celih brojeva. Time dobijamo sledeći program:
#include<stdio.h> #include<stdlib.h> main() { unsigned int x, y; unsigned int q, r; printf("Unesite brojeve x i y za koje zelite da izracunate celobrojno deljenje:\n"); scanf("%d%d", &x, &y); if(y == 0) { printf("Greska pri unosu vrednosti y!\n"); exit(1); } q = 0; r = x; while (r >= y) { q = q + 1; r = r - y; } printf("%d = %d * %d + %d\n", x, q, y, r); }
Ako iskoristimo specifičnosti programskog jezika C, prethodni program postaje:
#include<stdio.h> #include<stdlib.h> main() { unsigned int x, y, q, r; printf("Unesite brojeve x i y za koje zelite da izracunate celobrojno deljenje:\n"); scanf("%d%d", &x, &y); if(y == 0) { printf("Greska pri unosu vrednosti y!\n"); exit(1); } q = 0; r = x; while (r >= y) { q++; r -= y; } printf("%d = %d * %d + %d\n", x, q, y, r); }
Na ovaj način smo došli do kraja razvojnog puta programa za izračunavanje celog dela i ostatka pri celobrojnom deljenju prirodnih projeva x i y. Pri tome, znamo da se on uvek zaustavlja i da je korektan za sve vrednosti ulaznih parametara.
Naredna: Celobrojni koren Gore: Celobrojno deljenje Prethodna: Dokaz zaustavljanja programa Sadržaj