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

Jako niezmiennik pętli spróbujmy formułę $N\equiv i\le j\wedge \mathrm{\exists }x.i\le x\le j\wedge A[x]=v$.

$\{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)\}$
$\{N[j\mapsto n][i\mapsto 1]\}$
i := 1; 
j := n;
while   $\{N\}$  i < j do
(
  $\{N\wedge i<j\}$
  k := (i + j) div 2;
  $\{?\}$
  if A[k] < v then
  (
    $\{?\wedge A[k]<v\}$
    i := k + 1
    $\{N\}$
  )
  else
  (
    $\{?\wedge A[k]\ge v\}$
    j := k
    $\{N\}$
  ) 
  $\{N\}$
)
$\{N\wedge i\ge j\}$
$\{A[i]=v\}$

Oprócz samego niezmiennika, musimy też odgadnąć asercję, którą wpiszemy w miejsce znaku zapytania. Warunek, którego potrzebujemy to $N\wedge i\le k<j$.

$\{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)\}$
$\{N[j\mapsto n][i\mapsto 1]\}$
i := 1; 
j := n;
while  $\{N\}$  i < j do
(
  $\{N\wedge i<j\}$
    $\Downarrow$
  $\{N\wedge i\le (i+j)\mathrm{d}\mathrm{i}\mathrm{v}2<j\}$       // k nie występuje w $N$ 
  $\{N[k\mapsto (i+j)\mathrm{d}\mathrm{i}\mathrm{v}2]\wedge i\le (i+j)\mathrm{d}\mathrm{i}\mathrm{v}2<j\}$
  k := (i + j) div 2;
  $\{N\wedge i\le k<j\}$
  if A[k] < v then
  (
    $\{N\wedge i\le k<j\wedge A[k]<v\}$
    $\Downarrow$        // tutaj się nie uda! 
    $\{N[i\mapsto k+1]\}$
    i := k + 1
    $\{N\}$
  )
  else
  (
    $\{N\wedge i\le k<j\wedge A[k]\ge v\}$
    $\Downarrow$        // tutaj się tez ie uda! 
    $\{N[j\mapsto k]\}$
    j := k
    $\{N\}$
  ) 
  $\{N\}$
)
$\{N\wedge i\ge j\}$
    $\Downarrow$
$\{A[i]=v\}$

Niestety, nie potrafimy dowieść dwóch implikacji! Jest tak dlatego, że nasz niezmiennik jest za słaby i nie zawiera informacji o tym, że tablica jest posortowana! Oto poprawiony niezmiennik:

$N\equiv i\le j\wedge (\mathrm{\forall }x.1\le x<n⟹A[x]\le A[x+1])\wedge (\mathrm{\exists }x.i\le x\le j\wedge A[x]=v).$

Wciąż jest on jednak za słaby! Nie potrafimy skorzystać z wiedzy o tym, że A[1 .. n] jest posortowana, bo nie wiemy, czy $i,j$ należą do zakresu tablicy! Oto prawidłowy niezmiennik:

$N\equiv 1\le i\le j\le n\wedge (\mathrm{\forall }x.1\le x<n⟹A[x]\le A[x+1])\wedge (\mathrm{\exists }x.i\le x\le j\wedge A[x]=v).$

Ć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)

Oto program znajdujący znakomitość w czasie liniowym względem n:

i := 1; j := n;
while i <> j do
  if A[i, j] = 1 then      // i zna j więc i nie może być znakomitością 
    i := i + 1
  else      // i nie zna j więc j nie może być znakomitością 
    j := j - 1

Teraz musimy podać asercje specyfikujące poprawność częściową programu:

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

Zmieniliśmy warunek instrukcji warunkowej na "i zna j". Dzięki temu nie musimy wpisywać do asercji założenia $\mathrm{\forall }i,j.A[i,j]\in \{0,1\}$.

}}

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

Niezmiennik: $N\equiv i\le j\wedge (\mathrm{\exists }k.1\le k\le n\wedge k\text{ jest znakomitością})⟹(\mathrm{\exists }k.i\le k\le j\wedge k\text{ jest znakomitością}).$

$\{n\ge 1\}$
i := 1; j := n;
$\{N\}$
while  $\{N\}$  i <> j do
(
  $\{N\wedge i\ne j\}$
  if i zna j then
  (
    $\{N\wedge i\ne j\wedge i\text{ zna }j\}$
      $\Downarrow$
    $\{N[i\mapsto i+1]\}$
    i := i + 1
    $\{N\}$
  )
  else
  (
    $\{N\wedge i\ne j\wedge i\text{ nie zna }j\}$
    $\{N[j\mapsto j-1]\}$
    j := j - 1
    $\{N\}$
  )
  $\{N\}$
)
$\{N\wedge i=j\}$
$\{(\mathrm{\exists }k.1\le k\le n\wedge k\text{ jest znakomitością})⟹i\text{ jest znakomitością}\}$

Spójrzmy na jedną z implikacji (zaznaczoną w programie):

$N\wedge i\ne j\wedge i\text{ zna }j⟹N[i\mapsto i+1].$

Niemiennik $N$ zawiera w sobie zdanie warunkowe: "jeśli wśród 1 .. n istnieje znakomitość to ..". Zatem w dowodzie tej implikacji najpierw zakładamy przesłankę całej implikacji, a następnie zakładamy, że wśród 1 .. n istnieje znakomitość. Korzystając z tych dwóch założeń dowodzimy tezy: znakomitość jest wśród i+1 .. j.

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