Semantyka i weryfikacja programów/Ćwiczenia 14: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
← poprzednia edycjanastępna edycja →
WizualnieWikikod
Sl (dyskusja | edycje)
101 edycji
Nie podano opisu zmian
Sl (dyskusja | edycje)
101 edycji
Nie podano opisu zmian
Linia 71: Linia 71:
  (
  (
   <math>{\color{Red}\{N \land i < j\}}</math>
   <math>{\color{Red}\{N \land i < j\}}</math>
     <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// tutaj się nie uda! </span>
     <math>{\color{Green}\Downarrow}</math>
   <math>{\color{Red}\{N \land i \leq (i{+}j) \div 2 < j\}}</math>      <span style="color:brown">// k nie występuje w <math>N</math> </span>
   <math>{\color{Red}\{N \land i \leq (i{+}j) \,\mathrm{div}\, 2 < j\}}</math>      <span style="color:brown">// k nie występuje w <math>N</math> </span>
   <math>{\color{Red}\{N[k \mapsto (i{+}j) \div 2] \land i \leq (i{+}j) \div 2 < j\}}</math>
   <math>{\color{Red}\{N[k \mapsto (i{+}j) \,\mathrm{div}\, 2] \land i \leq (i{+}j) \,\mathrm{div}\, 2 < j\}}</math>
   k := (i + j) div 2;
   k := (i + j) div 2;
   <math>{\color{Red}\{ N \land i \leq k < j\}}</math>
   <math>{\color{Red}\{ N \land i \leq k < j\}}</math>
Linia 79: Linia 79:
   (
   (
     <math>{\color{Red}\{ N \land i \leq k < j \land A[k] < v\}}</math>
     <math>{\color{Red}\{ N \land i \leq k < j \land A[k] < v\}}</math>
     <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// tutaj też się nie uda! </span>
     <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// tutaj się nie uda! </span>
     <math>{\color{Red}\{N[i \mapsto k{+}1]\}}</math>
     <math>{\color{Red}\{N[i \mapsto k{+}1]\}}</math>
     i := k + 1
     i := k + 1
Linia 87: Linia 87:
   (
   (
     <math>{\color{Red}\{ N \land i \leq k < j \land A[k] \geq v\}}</math>
     <math>{\color{Red}\{ N \land i \leq k < j \land A[k] \geq v\}}</math>
     <math>{\color{Green}\Downarrow}</math>
     <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// tutaj się tez ie uda! </span>
     <math>{\color{Red}\{N[j \mapsto k]\}}</math>
     <math>{\color{Red}\{N[j \mapsto k]\}}</math>
     j := k
     j := k
Linia 107: Linia 107:
</math>
</math>


Wciąz jest on jednak za słaby!  
Wciąz 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 nalezą do zakresu tablicy! Oto prawidłowy niezmiennik:
Nie potrafimy skorzystać z wiedzy o tym, że A[1 .. n] jest posortowana, bo nie wiemy, czy i,j nalezą do zakresu tablicy!
Oto prawidłowy niezmiennik:


<math>
<math>
Linia 126: Linia 124:


* i zna j <math>\equiv</math> A[i, j] = 1
* i zna j <math>\equiv</math> A[i, j] = 1
* i nie zna j <math>\equiv</math> A[i, j] = 0
* i nie zna j <math>\equiv</math> A[i, j] = 0.


Powiemy, że i jest ''znakomitością'' jeśli zachodzi warunek:
Powiemy, że i jest ''znakomitością'' jeśli zachodzi warunek:
Linia 164: Linia 162:
   else
   else
     j := j - 1
     j := j - 1
  <math>{\color{Red}\{(exists k. 1 \leq k \leq n \land k \mbox{ jest znakomitością}) \implies i \mbox{ jest znakomitością}\}}</math>
  <math>{\color{Red}\{(\exists k. 1 \leq k \leq n \land k \mbox{ jest znakomitością}) \implies i \mbox{ jest znakomitością}\}}</math>




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


</div></div>
</div></div>
Linia 178: Linia 176:
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">


Niezmiennik <math>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ą}).</math>
Niezmiennik:
<math>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ą}).</math>




Linia 228: Linia 227:
{{cwiczenie|3 (algorytm zachłanny)|cw3|
{{cwiczenie|3 (algorytm zachłanny)|cw3|
Niech <math>G = (V, E)</math> będzie spójnym grafem nieskierowanym.
Niech <math>G = (V, E)</math> 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:
Załóżmy, że mamy do dyspozycji następujące struktury danych:


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


Graf reprezentowany jest przez dwie operacje pocz(e), kon(e) zwracające wierzchołek
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.
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:
Przeprowadź dowód poprawności częściowej programu obliczającego minimalne drzewo rozpinające:
Linia 251: Linia 252:
  <math>{\color{Red}\{G=(V,E) \mbox{ jest spójny}\}}</math>
  <math>{\color{Red}\{G=(V,E) \mbox{ jest spójny}\}}</math>
   
   
  P.inicjuj(V);
  // inicjuj P i Q j.w.
Q.inicjuj(E);
  T := <math>\emptyset</math>;
  T := <math>\emptyset</math>;
   
   
  while |P| > 1 do
  while |P| > 1 do
   e := deletemin(Q);
   e := min(Q);
  Q := deletemin(Q);
   x = pocz(e); y := kon(e);
   x = pocz(e); y := kon(e);
   X := P.find(x);
   X := find(P, x);
   Y := P.find(y);
   Y := find(P, y);
   
   
   if X <> Y then
   if X <> Y then
     T := T <math>\cup</math> {e};
     T := T <math>\cup</math> {e};
     P.union(X, Y)
     P := union(P, X, Y)
   
   
  <math>{\color{Red}\{T \mbox{ jest minimalnym drzewem rozpinającym graf } G\}}</math>
  <math>{\color{Red}\{T \mbox{ jest minimalnym drzewem rozpinającym graf } G\}}</math>
Linia 273: Linia 274:
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">


Tym razem niezmiennik pętli <math>N</math> jest niebanalną formułą, używającą operacji udostępnianych przez struktury danych:
Tym razem niezmiennik pętli <math>N</math> 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 <math>T</math>
* elementy kolejki <math>Q</math> należą do <math>E \setminus T</math>
* jeśli krawędź <math>e</math> nie należy do <math>Q</math>, to obydwa końce krawędzi e należą do tej samej klasy podziału <math>P</math>.


* T jest zawarte w pewnym minimalnym drzewie rozpinającym i
Ostatni warunek można też sformułować tak: jeśli krawędź <math>e</math> nie należy do <math>Q</math> i nie należy do drzewa <math>T</math>, to <math>T \cup \{e\}</math> ma cykl.
* 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, i
Oznacza to w szczególności, że krawędzi <math>e</math> na pewno nie możemy dodać do <math>T</math>.
* elementy kolejki Q zawarte należą do <math>E \setminus T</math>, i
* <math>\forall e \in E \setminus T. e \notin Q \implies</math> obydwa końce krawędzi e należą do tej samej klasy podziału P (czyli <math>T \cup \{e\}</math> ma cykl).




  <math>{\color{Red}\{G=(V,E) \mbox{ jest spójny}\}}</math>
  <math>{\color{Red}\{G=(V,E) \mbox{ jest spójny}\}}</math>
   
   
  P.inicjuj(V);
  // inicjuj P i Q j.w.
Q.inicjuj(E);
  T := <math>\emptyset</math>;
  T := <math>emptyset</math>;
  <math>{\color{Red}\{N\}}</math>
  <math>{\color{Red}\{N\}}</math>
  while |P| > 1 do
  while |P| > 1 do
  (
  (
   <math>{\color{Red}\{N \land |P| > 1\}}</math>
   <math>{\color{Red}\{N \land |P| > 1\}}</math>
   e := deletemin(Q);
   e := min(Q);
  Q := deletemin(Q);
   x = pocz(e); y := kon(e);
   x = pocz(e); y := kon(e);
   X := P.find(x);
   X := find(P, x);
   Y := P.find(y);
   Y := find(P, y);
   <math>{\color{Red}\{\alpha\}}</math>  
   <math>{\color{Red}\{\alpha\}}</math>  
   if X <> Y then
   if X <> Y then
   (
   (
     <math>{\color{Red}\{\alpha \land X <> Y\}}</math>
     <math>{\color{Red}\{\alpha \land X \neq Y\}}</math>
     <math>{\color{Red}\{N[P \mapsto P \setminus \{ X, Y \} \cup \{ X \cup Y \}][T \mapsto T \cup {e}]\}}</math>   
     <math>{\color{Red}\{N[P \mapsto P \setminus \{ X, Y \} \cup \{ X \cup Y \}][T \mapsto T \cup {e}]\}}</math>   
     T := T <math>\cup</math> {e};
     T := T <math>\cup</math> {e};
     P := P <math>\setminus</math> { X, Y <math>\cup</math> { X <math>\cup</math> Y }    <span style="color:brown">//  P := union(P, X, Y)  </span>
     P := P <math>\setminus</math> { X, Y <math>\cup</math> { X <math>\cup</math> Y }    <span style="color:brown">//  czyli P := union(P, X, Y)  </span>
     <math>{\color{Red}\{N\}}</math>   
     <math>{\color{Red}\{N\}}</math>   
   )
   )
Linia 315: Linia 320:
* X, Y są klasami abstrakcji końców krawędzi e.
* X, Y są klasami abstrakcji końców krawędzi e.


Skoncentrujmy się na instrukcji warunkowej.
Pierwszy z warunków łatwo jest zaakceptować wiedząc, że <math>\mathrm{add}(\mathrm{deletemin}(Q), \mathrm{min}(Q)) = Q</math>.
Należy pokazać dwie implikacje:
 
Skoncentrujmy się wyłącznie na instrukcji warunkowej. Należy pokazać dwie implikacje:


* <math>\alpha \land X <> Y \, \implies \, N[P \mapsto P \setminus \{ X, Y \} \cup \{ X \cup Y \}][T \mapsto T \cup {e}]</math>   
* <math>\alpha \land X \neq Y \, \implies \, N[P \mapsto P \setminus \{ X, Y \} \cup \{ X \cup Y \}][T \mapsto T \cup {e}]</math>   
* <math>\alpha \land X = Y \, \implies \, N</math>.
* <math>\alpha \land X = Y \, \implies \, N</math>.


Linia 377: Linia 383:




  <math>{\color{Red}\{n \geq 0 \land \odd(n)\}}</math>
  <math>{\color{Red}\{n \geq 0 \land \,\mathrm{odd}(n)\}}</math>
  k := A[1]; p := 1; i := 2;
  k := A[1]; p := 1; i := 2;
  while i <= n do
  while i <= n do
Linia 406: Linia 412:
   else
   else
     j := j - 1
     j := j - 1
  <math>{\color{Red}\{\mbox{ jest znakomitością}\}}</math>
  <math>{\color{Red}\{i \mbox{ jest znakomitością}\}}</math>

Wersja z 13:24, 16 sie 2006


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≥1∧(∀x.1≤x<n⟹A[x]≤A[x+1])∧(∃x.1≤x≤n∧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 ≡ A[i, j] = 1
  • i nie zna j ≡ A[i, j] = 0.

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

∀j.(1≤j≤n∧j≠i)⟹(j zna i∧i 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∪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) jest spójny}

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

{T 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≥1∧∀x.1≤x<n⟹A[x]≤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
{(∃x.1≤x≤n∧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≥1∧∀x.1≤x<n⟹A[x]≤A[x+1]}
i := 1; p := 0;
while i <= n do
  if A[i] = A[i - p] then
    p := p + 1;
  i := i + 1
{ maksymalna długość stałego odcinka w tablicy A 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≥0∧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
{ 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: 


{∃k.1≤k≤n∧k jest znakomitością}
i := 1; j := n;
while i <> j do
  if i zna j then
    i := i + 1
  else
    j := j - 1
{i jest znakomitością}
Źródło: „https://wazniak.mimuw.edu.pl/index.php?title=Semantyka_i_weryfikacja_programów/Ćwiczenia_14&oldid=19001”