Wstęp do programowania / Ćwiczenia 6

<<< Powrót do modułu Dowodzenie poprawności programów

To są zadania na logikę Hoare'a.

Oglądaj wskazówki i rozwiązania __SHOWALL__
Ukryj wskazówki i rozwiązania __HIDEALL__

Zadanie 1 (Flaga trójkolorowa)

Udowodnij częściową poprawność podanego poniżej rozwiązania zadania o fladze trójkolorowej.

Ćwiczenie

Dana jest tablica A typu array[1..N] of integer (N > 0). Należy tak poprzestawiać w niej elementy, żeby najpierw były elementy ujemne, potem równe zero, a na końcu dodatnie.

Program

program FlagaTrójkolorowa(N:integer; A:array[1..N] of integer);
var m,r,w,pom : integer;
begin
  m:=1; r:=1; w:=N;
  while r <= w do 
    if A[r]=0 then r:=r+1			//przedłużamy segment liczb dodatnich	
    else 
      if A[r]<0 then begin			
        pom:=A[r]; A[r]:=A[m]; A[m]:=pom;	//zamieniamy wartości w A[r] i A[m], po zamianie A[r]=0 i A[m] < 0  
        m:=m+1;					//więc zwiększamy oba indeksy r i m
        r:=r+1;
      end
      else begin
        pom:=A[r]; A[r]:=A[w]; A[w]:=pom;	//zamieniamy wartości w A[r] i A[w]
        w:=w-1;					//po zamianie A[w]>0,  ale o A[r] nic nie wiemy
      end;			     
end.

Rozwiązanie

Główną trudnością jest wymyślenie odpowiedniego niezmiennika pętli while. Tu będzie to zdanie:

∀ i  (1 ≤ i < m) ⇒  A[i] < 0 ∧   
∀ j  (m ≤ j < r) ⇒  A[j] = 0 ∧  
∀ k  (w < k ≤ N) ⇒  A[k] > 0 ∧   
1 ≤ m ≤ r ∧  r-1 ≤ w ≤ N ∧ N > 0

oznaczane przez N(m,r,w). Mówi ono, że na indeksach mniejszych od m są wartości ujemne, pomiędzy m a r - równe zero, a powyżej w - dodatnie. Nic nie jest powiedziane o wartościach tablicy pomiędzy r a w, za to wiemy jakie są relacje pomiędzy 1, m, r, w i N.

Poniżej znajduje się program wraz z anotacjami i dowody, że anotacje wraz z kodem który otaczają są poprawnymi trójkami Hoare'a.

  // N > 0 
1:m:=1; r:=1; w:=N;
  // N(m,r,w)
2:while r <= w do
  // N(m,r,w) ∧ r ≤ w 
3:  if A[r]=0 then 
      // N(m,r,w) ∧ r ≤ w ∧ A[r] = 0
      // N(m,r+1,w) 
4:    r:=r+1	
      // N(m,r,w)
5:   else 
6:    if A[r]<0 then begin
        // N(m,r,w) ∧ r ≤ w ∧ A[r] < 0			
7:      pom:=A[r]; A[r]:=A[m]; A[m]:=pom;	
        // N(m+1,r+1,w)
8:      m:=m+1; r:=r+1;
        // N(m,r,w)
      end
9:    else begin
        // N(m,r,w) ∧ r ≤ w ∧ A[r] > 0
10:     pom:=A[r]; A[r]:=A[w]; A[w]:=pom;	
        // N(m,r,w-1)  
11:     w:=w-1;	
        // N(m,r,w)			
12:   end;			     
  // N(m,r,w) ∧ r-1=w
 

1 Korzystamy z reguły na przypisanie. N(m,r,w) z wartościami m=1, r=1, w=1 jest równe

∀ i  (1 ≤ i < 1) ⇒  A[i] < 0 ∧   
∀ j  (m ≤ j < 1) ⇒  A[j] = 0 ∧  
∀ k  (N < j ≤ N) ⇒  A[k] > 0 ∧   
1 ≤ 1 ≤ 1 ∧  0 ≤ N ≤ N ∧ N > 0

i jest trywialnie prawdziwe.

2 Korzystamy z reguły na while; trzeba pokazać, że N(m,r,w) jest niezmiennikiem ciała pętli, czyli że zaczynając z N(m,r,w) ∧ r ≤ w po wykonaniu pętli zachodzi N(m,r,w).

3 Korzystamy z reguły na if; trzeba pokazać, że z N(m,r,w) ∧ r ≤ w po wykonaniu każdej gałęzi zachodzi N(m,r,w).

4 Korzystając z reguły na przypisanie, otrzymujemy, że N(m,r+1,w) powinno być prawdziwe przed instrukcją 4. Musimy więc dowieść implikacji

(N(m,r,w) ∧ r ≤ w ∧ A[r] = 0)  ⇒ N(m,r+1,w)

Rozpatrując części N(m,r+1,w) widzimy, że

∀ i  (1 ≤ i < m) ⇒  A[i] < 0 ∧   
∀ k  (w < j ≤ N) ⇒  A[k] > 0 ∧
1 ≤ m ∧ w ≤ N ∧ N > 0

wynikają trywialnie z N(m,r,w). Mamy też

∀ j  (m ≤ j < r+1) ⇒  A[j] = 0 

bo A[r] = 0.Ponieważ r ≤ w to

r+1-1 ∧ w

a ponieważ m ≤ r to

m ≤ r+1

5 W drugiej gałęzi instrukcji warunkowej z 3 znajduje się if. Schodząc do jego podgałęzi dodajemy do założeń, że A[r] <> 0.

6 Ciało podgałęzi spełniającej warunek A[r] < 0 składa się z dwóch grup przypisań.

7 Trzeba pokazać, że z N(m,r,w) ∧ r ≤ w ∧ A[r] < 0 wynika N(m+1,r+1,w) z zamienionymi wartościami A[r] i A[m]. Dokładniej, uzupełniając program o brakujące anotacje zgodnie z regułą na przypisanie, przed instrukcją A[m]:=pom mamy

∀ i  (1 ≤ i < m) ⇒  A[i] < 0 ∧ pom < 0  ∧   
∀ j  (m ≤ j < r) ⇒  A[j] = 0 ∧ A[r] = 0  ∧
∀ k  (w < j ≤ N) ⇒  A[k] > 0 ∧   
1 ≤ m+1 ≤ r+1 ∧ r ≤ w ≤ N ∧ N > 0

przed A[r]:=A[m]

∀ i  (1 ≤ i < m) ⇒  A[i] < 0 ∧ pom < 0  ∧   
∀ j  (m ≤ j < r) ⇒  A[j] = 0 ∧ A[m] = 0  ∧
∀ k  (w < j ≤ N) ⇒  A[k] > 0 ∧   
1 ≤ m+1 ≤ r+1 ∧ r ≤ w ≤ N ∧ N > 0

a przed pom:= A[r]

∀ i  (1 ≤ i < m) ⇒  A[i] < 0 ∧ A[r] < 0  ∧   
∀ j  (m ≤ j < r) ⇒  A[j] = 0 ∧ A[m] = 0  ∧
∀ k  (w < j ≤ N) ⇒  A[k] > 0 ∧   
1 ≤ m+1 ≤ r+1 ∧ r ≤ w ≤ N ∧ N > 0

czyli coś, co łatwo wynika z N(m,r,w) ∧ r ≤ w ∧ A[r] < 0.

8 Jest to trywialne użycie reguły na przypisanie.

9 Ciało podgałęzi spełniającej warunek A[r] > 0 składa się znów z dwóch grup przypisań.

10 Trzeba pokazać, że z N(m,r,w) ∧ r ≤ w ∧ A[r] > 0 wynika N(m,r,w-1) z zamienionymi wartościami A[r] i A[w] czyli

∀ i  (1 ≤ i < m) ⇒  A[i] < 0 ∧   
∀ j  (m ≤ j < r) ⇒  A[j] = 0 ∧  
∀ k  (w < k ≤ N) ⇒  A[k] > 0 ∧ A[r] > 0 ∧   
1 ≤ m ≤ r ∧
r-1 ≤ w-1 ≤ N ∧ N > 0

co jest łatwe.

11 Jest to trywialne użycie reguły na przypisanie.

12 Z reguły na while wiemy, że zachodzi N(m,r,w) i zaprzeczenie dozoru w while czyli r > w. Z niezmiennika wiemy, że r-1 ≤ w, musi więc być r-1=w.

Całkowita poprawność

Do udowodnienia całkowitej poprawności brakuje tylko argumentu, że program zawsze się zakończy, czyli że pętla zawsze się zakończy. Można w tym celu użyć miary (w-r)+1, ponieważ maleje ona w każdym obrocie pętli i jest zawsze nieujemna.

Zadanie 2 (Segment o danej sumie)

Udowodnij częściową poprawność dla podanego poniżej zadania i jego rozwiązania.

Ćwiczenie

Tablica A typu array[1..N] of integer, N >0 zawiera tylko liczby dodatnie. Napisz program, który dla danego W typu integer takiego, że W > 0 sprawdza, czy w A istnieje segment o sumie W (czyli czy istnieją l, p takie, że W$=A[l]+...+A[p-1]$).

Program

program SegmentODanejSumie2(N,W:integer; A:array[1..N] of integer);
//Tablica A zawiera tylko liczby dodatnie
var l,p,suma: integer;
    znalezione: boolean;
begin
  l:=1; p:=1;
  suma:=0;
  while (suma <> W) and (p <= N) do
    if suma < W then begin		//jeśli suma jest za mała, to przesuwamy prawy koniec segmentu
      suma:=suma+A[p];
      p:=p+1;
    end
    else begin			//jeśli za duża, to przesuwamy lewy koniec segmentu
      suma:= suma-A[l];
      l:=l+1;
    end;
  while (suma > W) do begin  
    suma:= suma-A[l];
    l:=l+1;
  end;
  znalezione:=(suma=W);
end.

Rozwiązanie

Zacznijmy od niezmiennika pierwszej pętli

∀ k  ∀ m (k < l ∧ l ≤ m ≤ N+1) ⇒  A[k]+...+A[m-1] <> W ∧
∀ m (l ≤ m < p) ⇒  A[l]+...+A[m-1] < W ∧   
1 ≤ l ≤ p ≤ N+1 ∧ N,W > 0 ∧ suma=A[l]+....A[p-1] ∧
A jest tablicą o wartościach dodatnich

oznaczanego przez N(l,p,suma). Mówi ono, że wszystkie segmenty o początku mniejszym od l i dowolnym końcu mają sumy różne od W, i że wszystkie segmenty o początku w l i końcu mniejszym od p mają sumy mniejsze niż W. Poza tym opisane są zależności między 1, l, p, N i suma.

Poniżej znajduje się program wraz z anotacjami i dowody, że anotacje wraz z kodem, który otaczają, są poprawnymi trójkami Hoare'a.

   // N,W > 0, A jest tablicą o wartościach dodatnich
1: l:=1; p:=1; suma:=0;
   // N(l,p,suma)
2: while (suma <> W) and (p <= N) do
     // N(l,p,suma) ∧ (suma <> W) ∧ (p ≤ N)
3:   if suma < W then begin
       // N(l,p,suma) ∧ (suma < W) ∧ (p ≤ N)	
4:     suma:=suma+A[p];
       p:=p+1;
       // N(l,p,suma)
     end
5:   else begin
       // N(l,p,suma) ∧ (suma > W) ∧ (p ≤ N)
6:     suma:= suma-A[l];
       l:=l+1;
       // N(l,p,suma)
7:   end;
     // N(l,p,suma) ∧ (suma=W ∨ p = N+1)
8:   while (suma > W) do begin  
       // N(l,p,suma) ∧ p = N+1 ∧ suma > W 
9:     suma:= suma-A[l];
       l:=l+1;
10:  end;
   // N(l,p,suma) ∧ (suma=W ∨ (p=N+1 ∧ suma < W))
11: znalezione:=(suma=W);
   //znalezione ⇔ (∃ l ∃ p 1 ≤ l ≤ p ≤ N+1 ∧ A[l]+...A[p-1] = W)  

1 Korzystamy z reguły na przypisanie. N(l,p,suma) z wartościami l=1, p=1, suma=0 jest równe

∀ k  ∀ m (k < 1 ∧ 1 ≤ m ≤ N+1) ⇒  A[k]+...+A[m-1] <> W ∧
∀ m (l ≤ m < 1) ⇒  A[l]+...+A[m-1] < W ∧   
1 ≤ 1 ≤ 1 ≤ N+1 ∧ N,W > 0 ∧ 0=0 ∧
A jest tablicą o wartościach dodatnich

i jest trywialnie prawdziwe.

2 Korzystamy z reguły na while; trzeba pokazać, że N(l,p,suma) jest niezmiennikiem ciała pętli, czyli że zaczynając z N(l,p,suma) ∧ suma <> W ∧ p ≤ N po wykonaniu pętli zachodzi N(l,p,suma).

3 Korzystamy z reguły na if; trzeba zrobić osobne sprawdzenia dla każdej gałęzi.

4 Zgodnie z regułą na przypisanie, musimy dowieść, że N(l,p,suma) ∧ (suma < W) ∧ (p ≤ N) wynika N(l,p+1,suma+A[p]),czyli

∀ k  ∀ m (k < l ∧ l ≤ m ≤ N+1) ⇒  A[k]+...+A[m-1] <> W ∧
∀ m (l ≤ m < p+1) ⇒  A[l]+...+A[m-1] < W ∧   
1 ≤ l ≤ p+1 ≤ N+1 ∧ N,W > 0 ∧ suma+A[p]=A[l]+....A[p] ∧
A jest tablicą o wartościach dodatnich

Jedyna część, która nie jest oczywista, to że A[l]+...A[p-1] < W, ale to wynika z (suma < W) i suma=A[l]+....A[p-1]

5 W drugiej gałęzi wiemy dodatkowo, że suma > W

6 Zgodnie z regułą na przypisanie, musimy dowieść, że N(l,p,suma) ∧ (suma > W) ∧ (p ≤ N) wynika N(l+1,p,suma-A[l]),czyli

∀ k  ∀ m (k < l+1 ∧ l+1 ≤ m ≤ N+1) ⇒  A[k]+...+A[m-1] <> W ∧
∀ m (l+1 ≤ m < p) ⇒  A[l+1]+...+A[m-1] < W ∧   
1 ≤ l+1 ≤ p ≤ N+1 ∧ N,W > 0 ∧
suma-A[l]=A[l+1]+....A[p-1] ∧
A jest tablicą o wartościach dodatnich

Spójrzmy najpierw na pierwszą linię niezmiennika: dla k < l, A[k]+...+A[m-1] <> W z założenia; dla k=l mamy pokazać że dla dowolnych m A[l]+...+A[m-1] <> W. Ale wiemy, że dla m < p+1 zachodzi A[l]+...A[m-1] < W i że A[l]+...A[p-1] > W (bo suma > W). Tym bardziej więc dla m > p+1 będzie A[l]+...A[m-1] > W (bo A jest dodatnia).

Dla uzasadnienia drugiej linii wystarczy zauważyć, że gdy skracamy segment o wartości mniejszej niż W, to jego wartość spada, bo A jest tablica dodatnią.

Pozostaje uzasadnienie l+1 ≤ p. Ponieważ suma > W to l < p, a więc też l+1 ≤ p.

7 Po pętli while wiemy, że zachodzi N(l,p,suma) i zaprzeczenie dozoru, czyli (suma=W ∨ p > N). Z niezmiennika wiemy, że p ≤ N+1, a więc musi być p=N+1.

8 Pokażemy, że N(l,p,suma) ∧ (suma=W ∨ p = N+1) jest niezmiennikiem tej pętli.

9 Zauważmy najpierw, że N(l,p,suma) ∧ (suma=W ∨ p = N+1) ∧ suma > W jest równoważne N(l,p,suma) ∧ p = N+1 ∧ suma > W.

Zgodnie z regułą na przypisanie, musimy dowieść, że N(l,p,suma) ∧ p = N+1 ∧ suma > W implikuje N(l+1,p,suma-A[l]) ∧ (suma-A[l]=W ∨ p = N+1). Zdanie N(l+1,p,suma-A[l]) dowodzi się tak, jak w punkcie 6. Ponieważ p =N+1, to zachodzi (suma-A[l]=W ∨ p = N+1).

10 Po wyjściu z pętli mamy N(l,p,suma) ∧ (suma=W ∨ p = N+1) i zaprzeczenie dozoru, czyli suma ≤ W, a więc N(l,p,suma) ∧ (suma=W ∨ (p=N+1 ∧ suma < W)).

11 Pozostaje udowodnić, że N(l,p,suma) ∧ (suma=W ∨ (p=N+1 ∧ suma < W)) implikuje (suma=W) ⇔ (∃ l ∃ p 1 ≤ l ≤ p ≤ N+1 ∧ A[l]+...A[p-1] = W) .

Jeśli suma=W to z N(l,p,suma), oczywiście wynika istnienie odpowiednich l i p. Jeśli suma <> W, to z założenia mamy p=N+1 i suma < W. I wtedy z niezmiennika wiemy, że

• segmenty o początkach mniejszych niż l mają sumy różne od W,
• segmenty o początkach w l i końcach mniejszych niż p mają sumy mniejsze niż W,
• segment o początku w l i końcu w p ma sumę mniejszą W,
• a więc też segmenty o początkach wiekszych od l i dowolnych końcach mają sumy mniejsze niż W.

Czyli nie isnieje segment o sumie równej W.

Całkowita poprawność

Do udowodnienia całkowitej poprawności brakuje tylko argumentu, że program zawsze się zakończy, czyli że obie pętle zawsze się zakończą. Dla pierwszej pętli można w tym celu użyć miary (2*N+1-p-l), ponieważ maleje ona w każdym obrocie pętli i jest zawsze nieujemna.

Dla drugiej pętli miarą jest suma+max(A[i] | i=1...N). Maleje ona w każdym obrocie pętli (bo tablica A jest dodatnia) i jest nieujemna.

Zadanie 3 (Głosowanie większościowe)

Udowodnij częściową poprawność dla podanego poniżej zadania i jego rozwiązania.

Ćwiczenie

Dana jest tablica A typu array[1..N] of integer, N > 0. Sprawdź, czy jest w niej element występujący więcej niż N/2 razy i jeśli tak, wskaż go.

Program

program Głosowanie2(N,W:integer; A:array[1..N] of integer);
var ile,i,kand,lider: integer;
begin
  kand:=A[1];		//szukamy kandydata na lidera
  ile := 1;
  i:=2;
  while i <= N do begin	
    if A[i]=kand then begin
      ile:=ile+1;
      i:=i+1;
    end
    else
      if ile > 0 then begin
        ile:=ile-1;
        i:=i+1;
      end
      else begin
        kand:=A[i];
        ile:=1;
        i:=i+1;
      end;
  end;
  ile:=0;		//sprawdzamy, czy kandydat jest liderem
  for i:=1 to n do 
    if A[i]=kand then ile:=ile+1; 
  if (ile >= (N div 2 + 1) then begin 
    lider:=kand;
    write('Liderem jest: ', kand);
  end 
  else 
    lider:=0;
end.

Rozwiązanie

Sprawdzenie, czy kandydat jest liderem, jest proste. Skoncentrujemy się więc na pierwszej części i wykażemy, że jeśli w tablicy jest lider to pierwsza część go znajduje.

Zacznijmy od niezmiennika pierwszej pętli oznaczanego przez N(i,ile,kand).

istnieje permutacja P:1..(i-1)->1..(i-1), taka że P(A[1..i-1])=kandile@ogon i 
ogon (rozpatrywany jako osobna tablica) nie ma lidera 
N > 0 ∧ 1 ≤ i ≤ N+1 ∧ ile ≥ 0

Poniżej znajduje się program wraz z anotacjami i dowody, że anotacje wraz z kodem, który otaczają, są poprawnymi trójkami Hoare'a.

   // N > 0
1: kand:=A[1];		
   ile := 1;
   i:=2;
   // N(i,ile,kand)
2: while i <= N do begin
     // N(i,ile,kand) ∧ i ≤ N
3:   if A[i]=kand then begin 
       // N(i,ile,kand) ∧ i ≤ N ∧ A[i]=kand 
4:     ile:=ile+1;
       i:=i+1;
       // N(i,ile,kand)
     end
     else
5:    if ile > 0 then begin
        // N(i,ile,kand) ∧ i ≤ N ∧ A[i] <> kand ∧ ile > 0  
6:      ile:=ile-1;
        i:=i+1;
        // N(i,ile,kand)
      end
      else begin
        // N(i,ile,kand) ∧ i ≤ N ∧ A[i] <> kand ∧ ile ≤ 0  
7:      kand:=A[i];
        ile:=1;
        i:=i+1;
        // N(i,ile,kand)
      end;
8: end;
   //Jeśli w tablicy istnieje lider to jest nim kand

1 Korzystając z reguły na przypisanie mamy pokazać, że N(1,1,A[1]). Szukana permutacja jest identycznościowa, reszta jest pusta, i oraz ile są w wymaganych zakresach.

2 Będziemy pokazywać, że N(i,ile,kand) jest niezmiennikiem pętli.

3 Trzeba osobno rozważyć gałęzie if.

4 Korzystając z reguły na przypisanie, mamy do pokazania, że N(i,ile,kand) ∧ i ≤ N ∧ A[i]=kand implikuje N(i+1,ile+1,kand). Jeśli P to permutacja z N(i,ile,kand), to szukana permutacja to P', gdzie P'(ile+1)=A[i], P'(i)=P(ile+1), P'(x)=P(x) dla x<>i lub x<>ile+1. Ogon pozostaje niezmieniony, czyli nadal nie ma tam lidera. Ponieważ i ≤ N to i+1 ≤ N+1; oczywiście ile > 0.

5 Kolejny if; dowód znów się rozgałęzia.

6 Korzystając z reguły na przypisanie, mamy do pokazania, że N(i,ile,kand) ∧ i ≤ N ∧ A[i]<> kand i ∧ ile > 0 implikuje N(i+1,ile-1,kand). Jeśli P to permutacja z N(i,ile,kand), to szukana permutacja to P rozszerzona o identyczność na i. W nowym ogonie mamy dodatkowo A[i] i kand. Z tego wynika, że gdyby A[i] był liderem w nowym ogonie, to A[i] byłby liderem w starym ogonie, co jest niemożliwe. Oczywiście i+1 ≤ N+1; oraz ile > 0.

7 Wpierw zauważmy, że ile ≤ 0 oraz ile ≥ 0 implikują ile=0. Korzystając z reguły na przypisanie, mamy do pokazania, że N(i,ile,kand) ∧ i ≤ N ∧ A[i] <> kand ∧ ile =0 implikuje N(i+1,1,A[i]). Ponieważ ile=0, to w tablicy A[1..i-1] nie ma lidera. Szukaną permutacją jest więc na przykład A[i]@A[1..i-1]. Oczywiście i+1 ≤ N+1; oraz ile > 0.

8 Po wyjściu z pętli mamy N(i,ile,kand) i zaprzeczenie dozoru, czyli i > N. To oznacza, że i=N+1. Czy możliwe jest, by liderem była wartość w <> kand? Jeśli tak przypuścimy, to niezależnie od ile, w musiałaby być liderem w ogonie, co jest sprzeczne z niezmiennikiem. Jedynym kandydatem na lidera jest więc rzeczywiście kand.

Zadanie 4 (BinPower)

Udowodnij częściową poprawność dla podanego poniżej zadania i jego rozwiązania.

Ćwiczenie

Dla zadanych x,n > 0 wyznacz xⁿ (oczywiscie bez exp i ln).

Program

function BinPower(x,n:integer):integer;
// Dla x,n > 0 wyznaczamy x do potęgi n 
var z,y,i: integer;
begin
  z:=1;
  y:=x;
  i:=n;
  while i > 0 do begin
    if (i mod 2 = 1) then z:=z*y;
    y:=y*y;
    i:=i div 2;
  end;
  BinPower:=z;
end;

Rozwiązanie

Zacznijmy od niezmiennika pętli oznaczanego przez N(z,y,i):

xn=z*yi ∧ i≥ 0

Poniżej znajduje się program wraz z anotacjami i dowody, że anotacje wraz z kodem, który otaczają, są poprawnymi trójkami Hoare'a.

   // x,n > 0
1: z:=1; y:=x; i:=n;
   // N(z,y,i)
2: while i > 0 do begin
     // N(z,y,i) ∧ i > 0
3:   if (i mod 2 = 1) then z:=z*y;
     // N(z,y*y,i div 2)
4:   y:=y*y;
     i:=i div 2;
     // N(z,y,i)
5: end;
   // z= xn

1 Korzystając z reguły na przypisanie, mamy pokazać, że N(1,x,n). Ponieważ n>0 to n≥ 0

2 Będziemy pokazywać, że N(z,y,i) jest niezmiennikiem pętli.

3 Choć mamy instrukcję if bez else, musimy pokazać dwie implikacje

N(z,y,i) ∧ i>0 ∧ i mod 2 = 1 ⇒ N(z*y, y*y, i div 2)
N(z,y,i) ∧ i>0 ∧ i mod 2 = 0 ⇒ N(z, y*y, i div 2)

Dla pierwszej z nich zauważmy, że jeśli i mod 2 = 1 to i=2*(i div 2) +1. Wtedy z*yⁱ= (z*y) * (y*y)^{(i div 2)}. Oczywiście jeśli i > 0 to i div 2 ≥ 0.

Dla drugiej mamy i=2*(i div 2). Wtedy z*yⁱ= z * (y*y)^{(i div 2)}. Podobnie, jeśli i > 0 to i div 2 ≥ 0.

4 Jest to dwa razy użyta reguła na przypisanie.

5 Po wyjściu z pętli mamy N(z,y,i) ∧ i ≤ 0. Ponieważ i ≥ 0 z niezmiennika, to i=0. A więc xⁿ=z.