Invarijanta petlje

Može se primetiti da je u svim test primerima nakon svake iteracije ispunjen uslov y=faktorijel(z) pa bi on mogao biti korisna invarijanta petlje.

Program u kojem je istaknuta (označena) potencijalna invarijanta zapisuje se na sledeći način:

 {x ≥ 0}
    y = 1;
    z = 0;
    {y = faktorijel(z)}
    while (z ≠ x) do 
      begin
         z = z + 1;
         y = y * z;
      {y = faktorijel(z)}
      end
{y = faktorijel(x)}

Pokažimo najpre da dati uslov važi nakon svake iteracije na prethodno pomenutim primerima.

Za x=4:

	x	y	z	y=faktorijel(z)
pre ulaska u petlju	4	1	0	1=faktorijel(0)
posle 1. iteracije	4	1	1	1=faktorijel(1)
posle 2. iteracije	4	2	2	2=faktorijel(2)
posle 3. iteracije	4	6	3	6=faktorijel(3)
posle 4. iteracije	4	24	4	24=faktorijel(4)

Za x=0:

	x	y	z	y=faktorijel(z)
pre ulaska u petlju	0	1	0	1=faktorijel(0)

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

{x ≥ 0}
  y = 1;
  z = 0;
&nbps;{y=faktorijel(z)}
  while (z ≠ x)
    begin
	z=z+1;
	y=y*z;
&nbps;{y=faktorijel(x)}
    end

Primer 1. Razmotrimo prethodno navedenu vezu u nešto drugačijem programu za x=4:

{x ≥ 0} 
    y = 1;
    z = 0;
    while (z ≠ x) do
      begin
         y = y * z;
         z = z + 1;
      end
{y = faktorijel(x)}

Može se primeti da već nakon prve iteracije odgovarajući uslov nije ispunjen, što znači da on nije invarijanta petlje ovog programa.

Primer 2. Uočimo šta se dešava u sledećem, na drugi način izmenjenom programu za x=4:

{x ≥ 0} 
    y = 1;
    z = 0;
    while (z ≤ x) do
      begin
         z = z + 1;
         y = y * z;
      end
{y = faktorijel(x)}

Nakon pete iteracije ulsov ulaska u petlju z ≤ x nije ispunjen jer ne važi 5 ≤ 4 pa se izvršavanje programa zaustavlja.

Kako 120 ≠ faktorijel(4) to pauslov programa nije zadovoljen što znači da ovaj program nije parcijalno korektan.