Semantyka i weryfikacja programów/Ćwiczenia 14

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania

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:



i := 1; j := n;
while i < j do
  k := (i + j) div 2;
  if A[k] < v then
    i := k + 1
  else
    j := k


Rozwiązanie


Ć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 A[i, j] = 1
  • i nie zna j A[i, j] = 0.

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

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)


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

Inne struktury danych

Ćwiczenie 3 (algorytm zachłanny)

Niech 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 i w jedną klasę
    • -- 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:




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

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  {e};
    P := union(P, X, Y)



Rozwiązanie (szkic)

P


Zadania domowe

Ćwiczenie 1

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



i := 1; j := n;
while i < j do
  k := (i + j) div 2;
  if A[k] < v then
    i := k + 1
  else
    j := k


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:



i := 1; p := 0;
while i <= n do
  if A[i] = A[i - p] then
    p := p + 1;
  i := i + 1


Ć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ę:



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


Ćwiczenie 4

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



i := 1; j := n;
while i <> j do
  if i zna j then
    i := i + 1
  else
    j := j - 1