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

Dana jest tablica dwuwymiarowa A[1 .. n, 1 .. n] zawierająca tylko liczby 0 i 1, reprezentująca relację znajomości pomiędzy n osobami. Umówmy się, że

• i zna j $\equiv$ A[i, j] = 1
• i nie zna j $\equiv$ A[i, j] = 0

Powiemy, że i jest znakomitością jeśli zachodzi warunek:

$\mathrm{\forall }j.(1\le j\le n\wedge j\ne i)⟹(j\text{ zna }i\wedge i\text{ nie zna }j)$

Napisz program znajdujący znakomitość, o ile istnieje. (Czy mogą być dwie różne znakomitości?) Przeprowadź dowód poprawności częściowej tego programu.

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$
  • $|P|$ -- liczba klas abstrakcji podziału.

Graf reprezentowany jest przez dwie operacje pocz(e), kon(e) zwracające wierzchołek będący oppowiednio początkiem i końcem krawędzi e.

Przeprowadź dowód poprawności częściowej programu obliczającego minimalne drzewo rozpinające:

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

P.inicjuj(V);
Q.inicjuj(E); 
T := $\mathrm{\varnothing }$;

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

Dana jest tablica A przechowująca wyniki wyborów: A[i] = j oznacza, że i głosował na j. Ordynacja wyborcza jest większościowa: zwycięzcą jest osoba, na którą głosowała przynajmniej połowa uprawnionych. Sformalizuj asercję końcową i przeprowadź dowód poprawności częściowej programu znajdującego zwycięzcę:

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ą}\}$