Specifikacija programa je ista kao i u primeru Celobrojno deljenje. Preduslov programa je {x ≥ 0, y > 0}. Na izlazu očekujemo vrednost celog dela q i ostatka r pri celobrojnom deljenju brojeva x i y, pa je pauslov {x = y * q + r, 0 ≤ r < y} . Dakle, specifikaciju našeg programa možemo zapisati na sledeći način:
{x ≥ 0, y > 0} --> {x = y * q + r, 0 ≤ r < y}
Ono što se u ovom primeru razlikuje je projektovanje i realizacija rešenja koje će biti efikasnije kao i način izvođenja invarijante petlje.
Naredna: Pseudokod programa Gore: Hardverdsko celobrojno deljenje Prethodna: Hardverdsko celobrojno deljenje Sadržaj