Semantyka i weryfikacja programów/Ćwiczenia 14

Zawartość

Kontynuujemy ćwiczenie dowodzenia poprawności częściowej prostych programów. Rozważymy programy operujące na tablicach i na innych strukturach danych.

Tablice

Ćwiczenie 1 (wyszukiwanie binarne)

Przeprowadź dowód poprawności częściowej poniższego programu:

$\{n\ge 1\wedge (\mathrm{\forall }x.1\le x<n⟹A[x]\le A[x+1])\wedge (\mathrm{\exists }x.1\le x\le n\wedge A[x]=v)\}$
i := 1; j := n;
while i < j do
  k := (i + j) div 2;
  if A[k] < v then
    i := k + 1
  else
    j := k
$\{A[i]=v\}$

Rozwiązanie

{{{3}}}

Ćwiczenie 2

{{{3}}}

Rozwiązanie (część pierwsza: program)

{{{3}}}

Rozwiązanie (część druga: dowód poprawności)

{{{3}}}

Inne struktury danych

Ćwiczenie 3 (algorytm zachłanny)

Niech $G=(V,E)$ będzie spójnym grafem nieskierowanym. Załóżmy, że mamy do dyspozycji następujące struktury danych:

• zbiór krawędzi grafu T, z operacjami:
  • inicjuj T jako zbiór pusty
  • dodaj nowy element do T
• kolejka priorytetowa krawędzi grafu Q, z operacjami:
  • inicjuj kolejkę za pomocą zbioru elementów (krawędzi)
  • deletemin(Q) usuwa z Q namniejszy element (krawędź) i zwraca go w wyniku
• podział zbioru wierzchołków P, z operacjami:
  • inicjuj P za pomocą zbioru wierzchołków jako podział jednoelementowych klas abstrakcji
  • find(x) zwraca klasę abstrakcji wierzchołka x
  • union(X, Y) łączy klasy $X$ i $Y$ w jedną klasę $X\cup Y$.

$\{G=(V,E)\text{ jest spójny}\}$

P.inicjuj(V);
Q.inicjuj(E); 
T := $emptyset$;

while |P| > 1 do
  e := deletemin(Q);
  x = pocz(e); y := kon(e);
  X := P.find(x);
  Y := P.find(y);

  if X <> Y then
    T := T $\cup$ {e};
    P.union(X, Y)

$\{T\text{ jest minimalnym drzewem rozpinającym graf }G\}$

Rozwiązanie (szkic)

P

Zadania domowe

Ćwiczenie 1

Przeprowadź jeszcze jeden dowód poprawności częściowej wyszukiwania binarnego.

$\{n\ge 1\wedge \mathrm{\forall }x.1\le x<n⟹A[x]\le A[x+1]\}$
i := 1; j := n;
while i < j do
  k := (i + j) div 2;
  if A[k] < v then
    i := k + 1
  else
    j := k
$\{(\mathrm{\exists }x.1\le x\le n\wedge A[x]=v)⟹A[i]=v\}$

Program pozostał ten sam, ale zmienione zostały asercje.

Ćwiczenie 2

Sformalizuj asercję końcową w poniższym programie i przeprowadź dowód poprawności częściowej:

$\{n\ge 1\wedge \mathrm{\forall }x.1\le x<n⟹A[x]\le A[x+1]\}$
i := 1; p := 0;
while i <= n do
  if A[i] = A[i - p] then
    p := p + 1;
  i := i + 1
$\{\text{ maksymalna długość stałego odcinka w tablicy }A\text{ wynosi }p\}$

Ćwiczenie 3

{{{3}}}

Parser nie mógł rozpoznać (nieznana funkcja „\odd”): {\displaystyle {\color{Red}\{n \geq 0 \land \odd(n)\}}}

k := A[1]; p := 1; i := 2;
while i <= n do
  if A[i] = k then
    p := p + 1;
  else
    if p > 1 then
      p := p - 1
    else
      k := A[i];
      p := 1;
  i := i + 1
$\{\text{ jeśli jest zwycięzca to jest nim }k\}$

Ćwiczenie 4

Przeprowadź jeszcze jeden dowód poprawności częściowej programu znajującego znakomitość, względem innych asercji:

$\{existsk.1\le k\le n\wedge k\text{ jest znakomitością}\}$
i := 1; j := n;
while i <> j do
  if i zna j then
    i := i + 1
  else
    j := j - 1
$\{\text{ jest znakomitością}\}$