Semantyka i weryfikacja programów/Ćwiczenia 14

From Studia Informatyczne

Spis treści

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:


{\color{Red}\{n \geq 1 \land (\forall x. 1 \leq x < n \implies A[x] \leq A[x+1]) \land (\exists x. 1 \leq x \leq n \land 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
{\color{Red}\{A[i] = v\}}


Rozwiązanie

Jako niezmiennik pętli spróbujmy formułę N \, \equiv \, i \leq j \land \exists x. i \leq x \leq j \land A[x] = v.


{\color{Red}\{n \geq 1 \land (\forall x. 1 \leq x < n \implies A[x] \leq A[x+1]) \land (\exists x. 1 \leq x \leq n \land A[x] = v)\}}
{\color{Red}\{N[j \mapsto n][i \mapsto 1]\}}
i := 1; 
j := n;
while   {\color{Red}\{N\}}  i < j do
(
  {\color{Red}\{N \land i < j\}}
  k := (i + j) div 2;
  {\color{Red}\{?\}}
  if A[k] < v then
  (
    {\color{Red}\{? \land A[k] < v\}}
    i := k + 1
    {\color{Red}\{N\}}
  )
  else
  (
    {\color{Red}\{? \land A[k] \geq v\}}
    j := k
    {\color{Red}\{N\}}
  ) 
  {\color{Red}\{N\}}
)
{\color{Red}\{N \land i \geq j\}}
{\color{Red}\{A[i] = v\}}


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


{\color{Red}\{n \geq 1 \land (\forall x. 1 \leq x < n \implies A[x] \leq A[x+1]) \land (\exists x. 1 \leq x \leq n \land A[x] = v)\}}
{\color{Red}\{N[j \mapsto n][i \mapsto 1]\}}
i := 1; 
j := n;
while  {\color{Red}\{N\}}  i < j do
(
  {\color{Red}\{N \land i < j\}}
    {\color{Green}\Downarrow}
  {\color{Red}\{N \land i \leq (i{+}j) \,\mathrm{div}\, 2 < j\}}       // k nie występuje w N 
  {\color{Red}\{N[k \mapsto (i{+}j) \,\mathrm{div}\, 2] \land i \leq (i{+}j) \,\mathrm{div}\, 2 < j\}}
  k := (i + j) div 2;
  {\color{Red}\{ N \land i \leq k < j\}}
  if A[k] < v then
  (
    {\color{Red}\{ N \land i \leq k < j \land A[k] < v\}}
    {\color{Green}\Downarrow}        // tutaj się nie uda! 
    {\color{Red}\{N[i \mapsto k{+}1]\}}
    i := k + 1
    {\color{Red}\{N\}}
  )
  else
  (
    {\color{Red}\{ N \land i \leq k < j \land A[k] \geq v\}}
    {\color{Green}\Downarrow}        // tutaj się tez ie uda! 
    {\color{Red}\{N[j \mapsto k]\}}
    j := k
    {\color{Red}\{N\}}
  ) 
  {\color{Red}\{N\}}
)
{\color{Red}\{N \land i \geq j\}}
    {\color{Green}\Downarrow}
{\color{Red}\{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 \leq j \land (\forall x. 1 \leq x < n \implies A[x] \leq A[x+1]) \land (\exists x. i \leq x \leq j \land 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 \leq i \leq j \leq n \land (\forall x. 1 \leq x < n \implies A[x] \leq A[x+1]) \land (\exists x. i \leq x \leq j \land 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:

\forall j. (1 \leq j \leq n \land j \neq i) \implies (j \mbox{ zna } i \, \land \, i \mbox{ 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:


{\color{Red}\{n \geq 1\}}
i := 1; j := n;
while i <> j do
  if i zna j then
    i := i + 1
  else
    j := j - 1
{\color{Red}\{(\exists k. 1 \leq k \leq n \land k \mbox{ jest znakomitością}) \implies i \mbox{ jest znakomitością}\}}


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


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

Niezmiennik:

N \, \equiv \, i \leq j \land (\exists k. 1 \leq k \leq n \land k \mbox{ jest znakomitością}) \implies (\exists k. i \leq k \leq j \land k \mbox{ jest znakomitością}).


{\color{Red}\{n \geq 1\}}
i := 1; j := n;
{\color{Red}\{N\}}
while  {\color{Red}\{N\}}  i <> j do
(
  {\color{Red}\{N \land i \neq j\}}
  if i zna j then
  (
    {\color{Red}\{N \land i \neq j \land i \mbox{ zna } j\}}
      {\color{Green}\Downarrow}
    {\color{Red}\{N[i \mapsto i{+}1]\}}
    i := i + 1
    {\color{Red}\{N\}}
  )
  else
  (
    {\color{Red}\{N \land i \neq j \land i \mbox{ nie zna } j\}}
    {\color{Red}\{N[j \mapsto j{-}1]\}}
    j := j - 1
    {\color{Red}\{N\}}
  )
  {\color{Red}\{N\}}
)
{\color{Red}\{N \land i = j\}}
{\color{Red}\{(\exists k. 1 \leq k \leq n \land k \mbox{ jest znakomitością}) \implies i \mbox{ jest znakomitością}\}}


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

N \land i \neq j \land i \mbox{ zna } j \, \implies \,  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:


{\color{Red}\{G=(V,E) \mbox{ jest spójny}\}}

// inicjuj P i Q j.w.
T := \emptyset;

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)

{\color{Red}\{T \mbox{ jest minimalnym drzewem rozpinającym graf } G\}}


Rozwiązanie (szkic)

Tym razem niezmiennik pętli N jest niebanalną formułą, używającą operacji udostępnianych przez struktury danych.

Zawiera on następujące zdania:

  • T jest zawarte w pewnym minimalnym drzewie rozpinającym
  • wierzchołki x, y należą do tej samej klasy abstrakcji podziału P wtw. gdy x i y są połączone ścieżką w T
  • elementy kolejki Q należą do E \setminus T
  • jeśli krawędź e nie należy do Q, to obydwa końce krawędzi e>/math> należą do tej samej klasy podziału <math>P.

Ostatni warunek można też sformułować tak: jeśli krawędź e nie należy do Q i nie należy do drzewa T, to T \cup \{e\} ma cykl. Oznacza to w szczególności, że krawędzi e na pewno nie możemy dodać do T.


{\color{Red}\{G=(V,E) \mbox{ jest spójny}\}}

// inicjuj P i Q j.w.
T := \emptyset;
{\color{Red}\{N\}}
while |P| > 1 do
(
  {\color{Red}\{N \land |P| > 1\}}
  e := min(Q);
  Q := deletemin(Q);
  x = pocz(e); y := kon(e);
  X := find(P, x);
  Y := find(P, y);
  {\color{Red}\{\alpha\}} 
  if X <> Y then
  (
    {\color{Red}\{\alpha \land X \neq Y\}}
    {\color{Red}\{N[P \mapsto P \setminus \{ X, Y \} \cup \{ X \cup Y \}][T \mapsto T \cup {e}]\}}  
    T := T \cup {e};
    P := P \setminus { X, Y \cup { X \cup Y }     //  czyli P := union(P, X, Y)  
    {\color{Red}\{N\}}  
  )
  {\color{Red}\{N\}}  
)
{\color{Red}\{N \land |P| = 1\}}  
{\color{Red}\{T \mbox{ jest minimalnym drzewem rozpinającym graf } G\}}


,,Zgadujemy" formułę \alpha:

  • N[Q \mapsto \mathrm{add}(Q, e)] i
  • e jest mniejsza niż wszystkie krawędzie z Q, i
  • X, Y są klasami abstrakcji końców krawędzi e.

Pierwszy z warunków łatwo jest zaakceptować wiedząc, że \mathrm{add}(\mathrm{deletemin}(Q), \mathrm{min}(Q)) = Q.

Skoncentrujmy się wyłącznie na instrukcji warunkowej. Należy pokazać dwie implikacje:

  • \alpha \land X \neq Y \, \implies \, N[P \mapsto P \setminus \{ X, Y \} \cup \{ X \cup Y \}][T \mapsto T \cup {e}]
  • \alpha \land X = Y \, \implies \, N.

Przykładowo, pierwsza implikacja wymaga wykazania, że T \cup \{ e \} jest podzbiorem minimalnego drzewa rozpinającego, wiedząc, że T jest takim podzbiorem, że e nie tworzy cyklu z krawędziami z T, oraz że e jest najmniejszą krawędzią o tej własności. Prawdziwość tego zdania wynika stąd, że poddzbiory drzew rozpinających stanowią strukturę zwaną matroidem. Pomijamy dalsze szczegóły.


Zadania domowe

Ćwiczenie 1

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


{\color{Red}\{n \geq 1 \land \forall x. 1 \leq x < n \implies A[x] \leq 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
{\color{Red}\{(\exists x. 1 \leq x \leq n \land A[x] = v) \implies 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:


{\color{Red}\{n \geq 1 \land \forall x. 1 \leq x < n \implies A[x] \leq A[x+1]\}}
i := 1; p := 0;
while i <= n do
  if A[i] = A[i - p] then
    p := p + 1;
  i := i + 1
{\color{Red}\{\mbox{ maksymalna długość stałego odcinka w tablicy } A \mbox{ 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ę:


{\color{Red}\{n \geq 0 \land \,\mathrm{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
{\color{Red}\{\mbox{ 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:


{\color{Red}\{\exists k. 1 \leq k \leq n \land k \mbox{ jest znakomitością}\}}
i := 1; j := n;
while i <> j do
  if i zna j then
    i := i + 1
  else
    j := j - 1
{\color{Red}\{i \mbox{ jest znakomitością}\}}