Wstęp do programowania / Ćwiczenia 6

Zadanie 1 (Flaga trójkolorowa)

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

Zadanie 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 < j ≤ N) ⇒  A[k] > 0 ∧   
1 ≤ m ≤ r ∧  r-1 ≤ w ≤ N ∧ N > 0

oznaczane przez N(m,r,w). 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. A więc musimy 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 < j ≤ 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, a więc musi 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.