Pseudokod programa sa istaknutim invarijantama

{x ≥ 0, y > 0}
q = 0
r = x;
z1 = y;
z2 = 1;
n = 0;
Tačka N:{z1 = y * z2}
while (z1 < r) do
  begin
    z1 = 2 * z1;
    z2 = 2 * z2;
    n = n + 1;
  {z1 = y * z2}
  end
if(z1 ≤ r)
  begin
    r = r - z1;
    q = q + z2;
  end 
m = 0;
Tačka M:{x = q * y + r, 0 ≤ r < z1}
while (z2 ≠ 1) do
  begin
    z1 = z1 / 2;
    z2 = z2 / 2;
    m = m + 1;
    if(r ≥ z1)
      begin
        r = r - z1;
        q = q + z2;
      end
  {x = q * y + r, 0 ≤ r < z1}
  end	
{x = q * y + r, 0 ≤ r < y}

Pratite izvršavanje programa i vrednosti invarijante za različite ulazne vrednosti

 
{x ≥ 0, y > 0}
 q = 0;
 r = x;
 z1 = y;
 z2 = 1;
 n = 0;
 {z1 = y * z2}
 while (z1 < r) do
      begin
        z1 = 2 * z1;
        z2 = 2 * z2;
        n = n + 1;
       {z1 = y * z2}
      end
 m = 0;
 if (z1 ≤ r) then
      begin
	r = r - z1;
	q = q + z2;
	...
 

Naredna: Dokaz zaustavljanja programa Gore: Hardverdsko celobrojno deljenje Prethodna: Izvođenje invarijanti   Sadržaj