Wstęp do programowania / Ćwiczenia 6

<<< Powrót do głównej strony wykładu

<<< Powrót do modułu 6

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

{{{3}}}

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

{{{3}}}

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.

Zadanie Dana jest tablica A typu array[1..N] of integer, N > 0. Sprawdź czyjest w niej element wystepują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 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 rozpatrzeć gałezie 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). Jesli 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 nie zmieniony 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). Jesli 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. A więc szukaną permutacją jest 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 mozliwe jest by liderem była wartośc w <> kand. Jeśli tak przypuścimy to niezależnie od ile, w musiałaby być liderem w ogonie, co jest sprzeczne z niezmiennikiem. a więc jedynym kandydatem an lidera jest rzeczywiście kand.

Zadanie 4 (BinPower)

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

Zadanie 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, ze 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.