Semantyka i weryfikacja programów/Ćwiczenia 15: 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
Dorota (dyskusja | edycje)
376 edycji
Nie podano opisu zmian
Linia 1: Linia 1:
== Zawartość ==
== Zawartość ==


Linia 29: Linia 28:
<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">


Intuicyjnie, pownniśmy wskazać wrażenie, którego wartość maleje w każdym obrocie pętli i jest zawsze nieujemna.
Intuicyjnie, pownniśmy wskazać wyrażenie, którego wartość maleje w każdym obrocie pętli i jest zawsze nieujemna.
Naturalnym kandydatem jest wyrażenie <math>q</math>.
Naturalnym kandydatem jest wyrażenie <math>q</math>.
W dowodzie poprawności częściowej używaliśmy niezmiennika <math>N \, \equiv \, z {\cdot} p^q = x^y</math>.
W dowodzie poprawności częściowej używaliśmy niezmiennika <math>N \, \equiv \, z {\cdot} p^q = x^y</math>.
Intuicyjnie mówiąc, dla własności stopu potrzebujemy dodatkowo własności <math>q \geq 0</math>, więc naturalnym pomysłem byłoby dodanie tej własności do niezmiennika.  
Intuicyjnie mówiąc, dla własności stopu potrzebujemy dodatkowo własności <math>q \geq 0</math>, więc naturalnym pomysłem byłoby dodanie tej własności do niezmiennika.  
Dla formalnego dowodu potrzebujemy jednak, ,,kontrolować" wartość zmiennej <math>q</math> za pomocą zewnętrzenego parametru:
Dla formalnego dowodu potrzebujemy jednak, "kontrolować" wartość zmiennej <math>q</math> za pomocą zewnętrzenego parametru:


<math>N'(l) \, \equiv \, z {\cdot} p^q = x^y \land q = l</math>.
<math>N'(l) \, \equiv \, z {\cdot} p^q = x^y \land q = l</math>.
Linia 54: Linia 53:
* <math>N'(0) \, \implies \, z = x^y</math>.
* <math>N'(0) \, \implies \, z = x^y</math>.


Zastosujemy teraz następującą regułe dla pętli (jest to odmiana reguły zaprezentowanej na wykładzie, która jest wygodna w tym zadaniu :)
Zastosujemy teraz następującą regułę dla pętli (jest to odmiana reguły zaprezentowanej na wykładzie, która jest wygodna w tym zadaniu :)


<math>
<math>
Linia 77: Linia 76:
* <math>N'(0) \implies q = 0</math>.
* <math>N'(0) \implies q = 0</math>.


Stosując teraz zwykłe reguły ,,przeciągamy" asercję <math>N'(l \,\mathrm{div}\, 2)</math> w tył:
Stosując teraz zwykłe reguły "przeciągamy" asercję <math>N'(l \,\mathrm{div}\, 2)</math> w tył:




Linia 102: Linia 101:
</math>
</math>


W przyszlości będziemy pomijać formalny dowód własności stopu i ograniczymy się do podania wyrażenia, które maleje w każdym obiegu pętli.
W przyszłości będziemy pomijać formalny dowód własności stopu i ograniczymy się do podania wyrażenia, które maleje w każdym obiegu pętli.
Będziemy używali następującej notacji:
Będziemy używali następującej notacji:


Linia 203: Linia 202:
Dwie zaznaczone implikacja są łatwe do udowodnienia.
Dwie zaznaczone implikacja są łatwe do udowodnienia.
Trudniej jest znależć niezmiennik dla pętli wewnętrznej.
Trudniej jest znależć niezmiennik dla pętli wewnętrznej.
Przede wszystkim zauważmy, że jeśli <math>N_1</math> ma się ,,odnawiać" po każdym obrocie zewnętrznej pętli, to wartość dodawana do zmiennej <math>s</math> powinna wynosić:
Przede wszystkim zauważmy, że jeśli <math>N_1</math> ma się "odnawiać" po każdym obrocie zewnętrznej pętli, to wartość dodawana do zmiennej <math>s</math> powinna wynosić:


<math>
<math>
Linia 211: Linia 210:
Zatem pętla wewnętrzna powinna prawdopodobnie obliczać na zmiennej <math>k</math> wartość <math>\frac{i {\cdot} (i+1)}{2} = 1 + 2 + \ldots + i</math>.
Zatem pętla wewnętrzna powinna prawdopodobnie obliczać na zmiennej <math>k</math> wartość <math>\frac{i {\cdot} (i+1)}{2} = 1 + 2 + \ldots + i</math>.
Jeśli uważnie przyjrzymy się pętli wewnętrznej, to zaobserwujemy, że zmienna <math>k</math> przechowuje wartość
Jeśli uważnie przyjrzymy się pętli wewnętrznej, to zaobserwujemy, że zmienna <math>k</math> przechowuje wartość
<math>1 + 2 + \ldots + l</math> plus ,,zaczęte" <math>l{+}1</math>, czyli plus <math>p</math>.
<math>1 + 2 + \ldots + l</math> plus "zaczęte" <math>l{+}1</math>, czyli plus <math>p</math>.
Spróbujmy niezmiennik postaci:
Spróbujmy niezmiennik postaci:


Linia 221: Linia 220:
Po pierwsze, zawsze zachodzi <math>p \leq l+1</math>.
Po pierwsze, zawsze zachodzi <math>p \leq l+1</math>.
Po drugie, oczekujemy, że spełniony będzie warunek <math>l < i</math>.  
Po drugie, oczekujemy, że spełniony będzie warunek <math>l < i</math>.  
Zauważmy, że zmienna l nigdy nie osiągnie wartości i, gdyż wcześniej zmienna p osiągnie tę wartość, a wtedy nastąpi od razu wyjście z pętli.
Zauważmy, że zmienna <math>l</math> nigdy nie osiągnie wartości <math>i</math>, gdyż wcześniej zmienna <math>p</math> osiągnie tę wartość, a wtedy nastąpi od razu wyjście z pętli.
Połączmy te ograniczenia w jeden zwięły warunek:
Połączmy te ograniczenia w jeden zwięły warunek:


Linia 285: Linia 284:


i wróćmy do ostatniej z implikacji powyżej. Wciąż brakuje nam pewnych informacji!  
i wróćmy do ostatniej z implikacji powyżej. Wciąż brakuje nam pewnych informacji!  
Tym razem nie potrafimy pokazac, że zachodzi <math>i{+}1 \leq n</math>, co stanowi część formuły <math>N_1[i \mapsto i{+}1][s \mapsto s {+} 6 {\cdot} k {+} p {-} l]</math>.
Tym razem nie potrafimy pokazać, że zachodzi <math>i{+}1 \leq n</math>, co stanowi część formuły <math>N_1[i \mapsto i{+}1][s \mapsto s {+} 6 {\cdot} k {+} p {-} l]</math>.
Powinniśmy dodać do <math>N_2</math> warunek <math>i < n</math>, który zachodzi zawsze po wejściu do pętli zewnętrznej.
Powinniśmy dodać do <math>N_2</math> warunek <math>i < n</math>, który zachodzi zawsze po wejściu do pętli zewnętrznej.
Otrzymujemy ostatecznie:
Otrzymujemy ostatecznie:
Linia 386: Linia 385:
<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">


Własność stopu pętli zewnętrznej łatwo jest pokazać, gdyż w każdym obiegu rośnie wartość zmiennej i, czyli maleje wartość wyrażenia <math>n - i</math>.
Własność stopu pętli zewnętrznej łatwo jest pokazać, gdyż w każdym obiegu rośnie wartość zmiennej <math>i</math>, czyli maleje wartość wyrażenia <math>n - i</math>.
Dodatkowo <math>n - i \geq 0</math> zagwarantowane jest przez niezmiennik <math>N_1</math>.
Dodatkowo <math>n - i \geq 0</math> zagwarantowane jest przez niezmiennik <math>N_1</math>.


Trudniej jest pokazać własność stopu pętli wewnętrznej.
Trudniej jest pokazać własność stopu pętli wewnętrznej.
Choć dozór tej pętli to <math>p < i</math>, to zasadnicze znaczenie dla tej pętli ma nie tyle wzrost wartości zmiennej p (zmienna i nie zmienia się w tej pętli) co wzrost wartości zmiennej l.
Choć dozór tej pętli to <math>p < i</math>, to zasadnicze znaczenie dla tej pętli ma nie tyle wzrost wartości zmiennej <math>p</math> (zmienna i nie zmienia się w tej pętli) co wzrost wartości zmiennej <math>l</math>.
Ale wyrażenie <math>i - l</math> nie maleje po każdym obiegu pętli!
Ale wyrażenie <math>i - l</math> nie maleje po każdym obiegu pętli!
Może ono pozostać niezmienione, ale wtedy rośnie na pewno wartość zmiennej p, czyli maleje <math>i - p</math>.
Może ono pozostać niezmienione, ale wtedy rośnie na pewno wartość zmiennej <math>p</math>, czyli maleje <math>i - p</math>.
Widać zatem, że warto tutaj wziąc pod uwagę porządek leksykograficzny par liczb: para wartości wyrażeń <math>\langle i - l, i - p \rangle</math>
Widać zatem, że warto tutaj wziąć pod uwagę porządek leksykograficzny par liczb: para wartości wyrażeń <math>\langle i - l, i - p \rangle</math>
maleje w porządku leksykograficznym po każdym obiegu pętli.
maleje w porządku leksykograficznym po każdym obiegu pętli.
Obydwa mają przy tym zawsze wartość większą lub równą 0, dzięki niezmiennikowi <math>N_2</math>.
Obydwa mają przy tym zawsze wartość większą lub równą 0, dzięki niezmiennikowi <math>N_2</math>.

Wersja z 15:20, 29 wrz 2006

Zawartość

Ostatnie ćwiczenia poświęcone będa dowodzeniu poprawności całkowitej programów.


Poprawność całkowita

Ćwiczenie 1 (potęgowanie binarne)

Przeprowadź dowód poprawności całkowitej (poprawność częściowa plus własność stopu) potęgowania binarnego: 


[y≥0]
z := 1; p := x; q := y;
while q <> 0 do
  if odd(q) then
    z := z * p;
  q := q div 2;
  p := p * p
[z=xy]


Rozwiązanie

{{{3}}}


Ćwiczenie 2

Przeprowadź dowód poprawności całkowitej poniższego programu. 


{n≥0}

s := 1; i := 1;
while i < n do
  k := 1; l := 0; p := 1;
  while p < i do
    k := k + 1;
    if l < p then
      l := l + 1;
      p := 1
    else
      p := p + 1;
  s := s + 6 * k + p - l;
  i := i + 1;
 
{s=n3}


Wskazówka

(m+1)3=m3+3⋅m2+3⋅m+1

Σj=1mj=m⋅(m+1)2


Rozwiązanie (poprawność częściowa)

{{{3}}}

Rozwiązanie (poprawność calkowita)

{{{3}}}


Zadania domowe

Ćwiczenie 1

Przeprowadź dowód poprawności całkowitej poniższego programu. 


[(∀x.1≤x<n⟹A[x]≤A[x+1])∧(∀x.n+1≤x<2⋅n⟹A[x]≤A[x+1])]
i := 1; j := 2 * n;
while A[i] < A[j] do
  ,,zamień A[i] i A[j]";
  i := i + 1;
  j := j - 1;
[∀x,y.1≤x≤n<y≤2⋅n⟹A[x]≥A[y]]
Źródło: „https://wazniak.mimuw.edu.pl/index.php?title=Semantyka_i_weryfikacja_programów/Ćwiczenia_15&oldid=59868”