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. Krawędziom grafu przypisane są różnowartościowo wagi liczbowe (czyli nie ma dwóch różnych krawędzi o tej samej wadze). Załóżmy, że mamy do dyspozycji następujące struktury danych:

• zbiór T krawędzi grafu, z operacjami:
  • inicjuj T jako zbiór pusty
  • dodaj nowy element do T
• kolejka priorytetowa Q przechowująca krawędzie grafu, z operacjami:
  • inicjuj kolejkę za pomocą zbioru wszystkich krawędzi grafu
  • add(Q, e): dodaj krawędż e do Q
  • deletemin(Q): usuń z Q namniejszy element (krawędź)
  • min(Q): zwróć w wyniku najmniejszy element (krawędź) w Q
• podział P zbioru wierzchołków grafu, z operacjami:
  • inicjuj P jako zbiór jednoelementowych klas abstrakcji, po jednej dla każdego wierzchołka grafu
  • find(P, x): zwróć klasę abstrakcji wierzchołka x
  • union(P, X, Y): połącz klasy abstrakcji $X$ i $Y$ w jedną klasę $X\cup Y$
  • $|P|$ -- zwróć liczbę klas abstrakcji podziału P.

Graf reprezentowany jest przez dwie operacje pocz(e), kon(e) zwracające wierzchołki będące odpowiednio 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}\}$

// inicjuj P i Q j.w.
T := $\mathrm{\varnothing }$;

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

  if X <> Y then
    T := T $\cup$ {e};
    P := union(P, 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ę:

$\{n\ge 0\wedge \mathrm{o}\mathrm{d}\mathrm{d}(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 znajdującego znakomitość względem innych asercji:

$\{\mathrm{\exists }k.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
$\{i\text{ jest znakomitością}\}$