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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
następna edycja →
WizualnieWikikod
Sl (dyskusja | edycje)
101 edycji
Nie podano opisu zmian
 
Sl (dyskusja | edycje)
101 edycji
Nie podano opisu zmian
Linia 123: Linia 123:
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.
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
Umówmy się, że
}}


* i zna j <math>\equiv</math> A[i, j] = 1
* i zna j <math>\equiv</math> A[i, j] = 1
Linia 135: Linia 136:
Napisz program znajdujący znakomitość, o ile istnieje. (Czy mogą być dwie różne znakomitości?)
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.
Przeprowadź dowód poprawności częściowej tego programu.
}}




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


Linia 187: Linia 187:
  i := 1; j := n;
  i := 1; j := n;
  <math>{\color{Red}\{N \\,\mathbf{end}AS
  <math>{\color{Red}\{N \\,\mathbf{end}AS
  while  <math>{\color{Red}\{N \\,\mathbf{end}AS i <> j do
  while  <math>{\color{Red}\{N\}}</math> i <> j do
  (
  (
   <math>{\color{Red}\{N \land i \neq j \\,\mathbf{end}AS
   <math>{\color{Red}\{N \land i \neq j\}}</math>
   if i zna j then
   if i zna j then
   (
   (
     <math>{\color{Red}\{N \land i \neq j \land i \mbox{ zna } j \\,\mathbf{end}AS
     <math>{\color{Red}\{N \land i \neq j \land i \mbox{ zna } j\}}</math>
       <math>{\color{Green}\Downarrow}</math>
       <math>{\color{Green}\Downarrow}</math>
     <math>{\color{Red}\{N[i \mapsto i{+}1] \\,\mathbf{end}AS
     <math>{\color{Red}\{N[i \mapsto i{+}1]\}}</math>
     i := i + 1
     i := i + 1
     <math>{\color{Red}\{N \\,\mathbf{end}AS
     <math>{\color{Red}\{N\}}</math>
   )
   )
   else
   else
   (
   (
     <math>{\color{Red}\{N \land i \neq j \land i \mbox{ nie zna } j \\,\mathbf{end}AS
     <math>{\color{Red}\{N \land i \neq j \land i \mbox{ nie zna } j\}}</math>
     <math>{\color{Red}\{N[j \mapsto j{-}1] \\,\mathbf{end}AS
     <math>{\color{Red}\{N[j \mapsto j{-}1]\}}</math>
     j := j - 1
     j := j - 1
     <math>{\color{Red}\{N \\,\mathbf{end}AS
     <math>{\color{Red}\{N\}}</math>
   )
   )
   <math>{\color{Red}\{N \\,\mathbf{end}AS
   <math>{\color{Red}\{N\}}</math>
  )
  )
  <math>{\color{Red}\{N \land i = j \\,\mathbf{end}AS
  <math>{\color{Red}\{N \land i = j\}}</math>
  <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>


Linia 242: Linia 242:
** inicjuj P za pomocą zbioru wierzchołków jako podział jednoelementowych klas abstrakcji
** inicjuj P za pomocą zbioru wierzchołków jako podział jednoelementowych klas abstrakcji
** find(x) zwraca klasę abstrakcji wierzchołka x
** find(x) zwraca klasę abstrakcji wierzchołka x
** union(X, Y) łączy klasy <math>X</math> i <math>Y</math> w jedną klasę <math>X \cup Y</math>.
** union(X, Y) łączy klasy <math>X</math> i <math>Y</math> w jedną klasę <math>X \cup Y</math>
** |P| -- liczba klas abstrakcji podziału
** <math>|P|</math> -- liczba klas abstrakcji podziału.


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łek
Linia 256: Linia 256:
  P.inicjuj(V);
  P.inicjuj(V);
  Q.inicjuj(E);  
  Q.inicjuj(E);  
  T := <math>emptyset</math>;
  T := <math>\emptyset</math>;
   
   
  while |P| > 1 do
  while |P| > 1 do
Linia 374: Linia 374:


{{cwiczenie|3|cw3.dom|
{{cwiczenie|3|cw3.dom|
}}
Dana jest tablica A przechowująca wyniki wyborów: A[i] = j oznacza, że i głosował na j.
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.
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ę:
Sformalizuj asercję końcową i przeprowadź dowód poprawności częściowej programu znajdującego zwycięzcę:
}}




Wersja z 08:26, 14 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. Załóżmy, że mamy do dyspozycji następujące struktury danych:

  • zbiór krawędzi grafu T, z operacjami:
    • inicjuj T jako zbiór pusty
    • dodaj nowy element do T
  • kolejka priorytetowa krawędzi grafu Q, z operacjami:
    • inicjuj kolejkę za pomocą zbioru elementów (krawędzi)
    • deletemin(Q) usuwa z Q namniejszy element (krawędź) i zwraca go w wyniku
  • podział zbioru wierzchołków P, z operacjami:
    • inicjuj P za pomocą zbioru wierzchołków jako podział jednoelementowych klas abstrakcji
    • find(x) zwraca klasę abstrakcji wierzchołka x
    • union(X, Y) łączy klasy X i Y w jedną klasę X∪Y
    • |P| -- liczba klas abstrakcji podziału.

Graf reprezentowany jest przez dwie operacje pocz(e), kon(e) zwracające wierzchołek 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: 


{G=(V,E) jest spójny}

P.inicjuj(V);
Q.inicjuj(E); 
T := ∅;

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

  if X <> Y then
    T := T ∪ {e};
    P.union(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ę: 


Parser nie mógł rozpoznać (nieznana funkcja „\odd”): {\displaystyle {\color{Red}\{n \geq 0 \land \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: 


{existsk.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
{ jest znakomitością}
Źródło: „https://wazniak.mimuw.edu.pl/index.php?title=Semantyka_i_weryfikacja_programów/Ćwiczenia_14&oldid=16133”