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 178: Linia 178:
<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  
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>
<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>




  <math>{\color{Red}\{n \geq 1\}}</math>
  <math>{\color{Red}\{n \geq 1\}}</math>
  i := 1; j := n;
  i := 1; j := n;
  <math>{\color{Red}\{N \\,\mathbf{end}AS
  <math>{\color{Red}\{N\}}</math>
  while  <math>{\color{Red}\{N\}}</math>  i <> j do
  while  <math>{\color{Red}\{N\}}</math>  i <> j do
  (
  (
Linia 208: Linia 205:
  )
  )
  <math>{\color{Red}\{N \land i = j\}}</math>
  <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 402: Linia 399:




  <math>{\color{Red}\{exists k. 1 \leq k \leq n \land k \mbox{ jest znakomitością}\}}</math>
  <math>{\color{Red}\{\exists k. 1 \leq k \leq n \land k \mbox{ jest znakomitością}\}}</math>
  i := 1; j := n;
  i := 1; j := n;
  while i <> j do
  while i <> j do

Wersja z 08:30, 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: 


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