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.

Wskazówka 1

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)
    else 
5:    if A[r]<0 then begin
        // N(m,r,w) ∧ r ≤ w ∧ A[r] < 0			
6:      pom:=A[r]; A[r]:=A[m]; A[m]:=pom;	
        // N(m+1,r+1,w) ∧ r ≤ w 
7:      m:=m+1; r:=r+1;
        // N(m,r,w)
      end
8:    else begin
        // N(m,r,w) ∧ r ≤ w ∧ A[r] > 0
9:      pom:=A[r]; A[r]:=A[w]; A[w]:=pom;	
        // N(m,r,w-1) ∧ r ≤ w 
10:     w:=w-1;	
        // N(m,r,w)			
11:   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

1. Korzystamy z reguły na while; trzeba pokazać, że N(m,r,w) jest niezmiennikiem ciała pętli, czyli że z N(m,r,w) ∧ r ≤ w po wykonaniu pętli zachodzi N(m,r,w)
2. Korzystamy z reguły na if; trzeba pokazać, że z N(m,r,w) ∧ r ≤ w po wykonaniu każdej gałęzi if-a zachodzi N(m,r,w)
3. 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)

N(m,r,w) z wstawionym r+1 na miejsce r ma postać

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

z czego trywialnie wynika

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

Brakuje

co jest równoważne

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