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

{{{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.

Ćwiczenie

Dana jest tablica A typu array[1..N] of integer, N > 0. Sprawdź, czy jest 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

{{{3}}}

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

{{{3}}}