Invarijanta petlje (izvođenje iz brojača)

Ovaj program ima dve petlje, jednu za drugom. Jedna mogućnost je da se pretpostavi šta bi mogle biti korisne invarijante petlji i da se onda dokaže da one to zaista jesu. Druga mogućnost, koju ćemo razmotriti u nastavku, je uvođenje brojača u petlje i izvođenje invarijanti na osnovu tih brojača. Neka je n brojač za prvu i neka je m brojač za drugu petlju.

Sada je pseudokod programa:

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

Izvedimo invarijante ovih petlji.

• Izvođenje invarijanti
• Pseudokod programa sa istaknutim invarijantama

Naredna: Izvođenje prve invarijante Gore: Hardverdsko celobrojno deljenje Prethodna: Pseudokod programa   Sadržaj