Semantyka i weryfikacja programów/Ćwiczenia 15: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 32: | Linia 32: | ||
Intuicyjnie, pownniśmy wskazać wrażenie, którego wartość maleje w każdym obrocie pętli i jest zawsze nieujemna. | Intuicyjnie, pownniśmy wskazać wraż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. | |||
Dla formalnego dowodu potrzebujemy jednak, ,,kontrolować" wartość zmiennej <math>q</math> za pomocą zewnętrzenego parametru: | |||
Dla formalnego dowodu | |||
<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>. | ||
Formalnie rzecz biorąc, wykażemy: | Formalnie rzecz biorąc, wykażemy: | ||
| Linia 56: | Linia 55: | ||
* <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 :) | |||
<math> | <math> | ||
\frac{l | \frac{l > 0 \land N'(l) \implies b \quad {\color{Red}[l > 0 \land N'(l)]} I {\color{Red}[N'(l \,\mathrm{div}\, 2)]} \quad N'(0) \implies \neg b} | ||
{{\color{Red}[\exists l. l \geq 0 \land N'(l)]} \mathbf{while}\, b \,\mathbf{do}\, I {\color{Red}[N'(0)]}} | {{\color{Red}[\exists l. l \geq 0 \land N'(l)]} \mathbf{while}\, b \,\mathbf{do}\, I {\color{Red}[N'(0)]}} | ||
</math> | </math> | ||
Wystarczy zatem dowieść: | |||
<math>{\color{Red}[l | <math>{\color{Red}[l > 0 \land N'(l)]}</math> | ||
if odd(q) then | if odd(q) then | ||
z := z * p; | z := z * p; | ||
| Linia 79: | Linia 78: | ||
* <math>N'(0) \implies q = 0</math>. | * <math>N'(0) \implies q = 0</math>. | ||
Stosując teraz zwykłe reguły ,,przeciągamy" | Stosując teraz zwykłe reguły ,,przeciągamy" asercję <math>N'(l \,\mathrm{div}\, 2)</math> w tył: | ||
<math>{\color{Red}[l | <math>{\color{Red}[l > 0 \land z {\cdot} p^q = x^y \land q = l]}</math> | ||
if odd(q) then | if odd(q) then | ||
( | ( | ||
<math>{\color{Red}[l | <math>{\color{Red}[l > 0 \land z {\cdot} p^q = x^y \land q = l \land \,\mathrm{odd}(q)]}</math> | ||
<math>{\color{Green}\Downarrow}</math> | <math>{\color{Green}\Downarrow}</math> | ||
<math>{\color{Red}[(z \cdot p) \cdot (p \cdot p)^(q \,\mathrm{div}\, 2) = x^y \land q \,\mathrm{div}\, 2 = l \,\mathrm{div}\, 2]}</math> | <math>{\color{Red}[(z {\cdot} p) {\cdot} (p {\cdot} p)^{(q \,\mathrm{div}\, 2)} = x^y \land q \,\mathrm{div}\, 2 = l \,\mathrm{div}\, 2]}</math> | ||
z := z * p; | z := z * p; | ||
<math>{\color{Red}[z \cdot (p \cdot p)^(q \,\mathrm{div}\, 2) = x^y \land q \,\mathrm{div}\, 2 = l \,\mathrm{div}\, 2]}</math> | <math>{\color{Red}[z {\cdot} (p {\cdot} p)^{(q \,\mathrm{div}\, 2)} = x^y \land q \,\mathrm{div}\, 2 = l \,\mathrm{div}\, 2]}</math> | ||
) | ) | ||
<math>{\color{Red}[z \cdot (p \cdot p)^(q \,\mathrm{div}\, 2) = x^y \land q \,\mathrm{div}\, 2 = l \,\mathrm{div}\, 2]}</math> | <math>{\color{Red}[z {\cdot} (p {\cdot} p)^{(q \,\mathrm{div}\, 2)} = x^y \land q \,\mathrm{div}\, 2 = l \,\mathrm{div}\, 2]}</math> | ||
q := q div 2; | q := q div 2; | ||
<math>{\color{Red}[z \cdot (p \cdot p)^q = x^y \land q = l \,\mathrm{div}\, 2]}</math> | <math>{\color{Red}[z {\cdot} (p {\cdot} p)^q = x^y \land q = l \,\mathrm{div}\, 2]}</math> | ||
p := p * p | p := p * p | ||
<math>{\color{Red}[z \cdot p^q = x^y \land q = l \,\mathrm{div}\, 2]}</math> | <math>{\color{Red}[z {\cdot} p^q = x^y \land q = l \,\mathrm{div}\, 2]}</math> | ||
W przyszlości będziemy pomijać formalny dowód własności | Oprócz implikacji zaznaczonej w anotacjach, powinniśmy też udowodnić: | ||
<math> | |||
l > 0 \land z {\cdot} p^q = x^y \land q = l \land \neg \,\mathrm{odd}(q) \, \implies \, z {\cdot} (p {\cdot} p)^{(q \,\mathrm{div}\, 2)} = x^y \land q \,\mathrm{div}\, 2 = l \,\mathrm{div}\, 2. | |||
</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. | |||
Będziemy używali następującej notacji: | Będziemy używali następującej notacji: | ||
| Linia 111: | Linia 116: | ||
p := p * p | p := p * p | ||
) | ) | ||
<math>{\color{Red}[N \land | <math>{\color{Red}[N \land q = 0]}</math> | ||
... | ... | ||
| Linia 149: | Linia 154: | ||
(m + 1)^3 \, = \, m^3 + 3 {\cdot} m^2 + 3 {\cdot} m + 1 | (m + 1)^3 \, = \, m^3 + 3 {\cdot} m^2 + 3 {\cdot} m + 1 | ||
</math> | </math> | ||
<math> | <math> | ||
\Sigma_{j = 1}^m \, = \, \frac{m \cdot (m+1)}{2} | \Sigma_{j = 1}^m j \, = \, \frac{m {\cdot} (m+1)}{2} | ||
</math> | </math> | ||
}} | }} | ||
| Linia 201: | Linia 207: | ||
<math> | <math> | ||
(i+1)^3 - i^3 = 3 \cdot | (i+1)^3 - i^3 = 3 {\cdot} i^2 + 3 {\cdot} i + 1 = 3 {\cdot} (i^2 + i) + 1 = 3 {\cdot} i {\cdot} (i{+}1) + 1. | ||
</math> | </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>. | 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" l+1, 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: | ||
<math> | <math> | ||
N_2 \, \equiv \, k = (1 + 2 + \ldots l) + p \land \ldots | N_2 \, \equiv \, k = (1 + 2 + \ldots + l) + p \land \ldots | ||
</math> | </math> | ||
| Linia 220: | Linia 226: | ||
<math> | <math> | ||
N_2 \, \equiv \, k = (1 + 2 + \ldots l) + p \land 1 \leq p \leq l+1 \leq i. | N_2 \, \equiv \, k = (1 + 2 + \ldots + l) + p \land 1 \leq p \leq l+1 \leq i. | ||
</math> | </math> | ||
| Linia 255: | Linia 261: | ||
<math>{\color{Red}\{N_2 \land p \geq i\}}</math> | <math>{\color{Red}\{N_2 \land p \geq i\}}</math> | ||
<math>{\color{Green}\Downarrow}</math> <span style="color:brown">// 4 </span> | <math>{\color{Green}\Downarrow}</math> <span style="color:brown">// 4 </span> | ||
<math>{\color{Red}\{N_1[i \mapsto i{+}1][s \mapsto s {+} 6 \cdot k {+} p {-} l]\}}</math> | <math>{\color{Red}\{N_1[i \mapsto i{+}1][s \mapsto s {+} 6 {\cdot} k {+} p {-} l]\}}</math> | ||
s := s + 6 * k + p - l; | s := s + 6 * k + p - l; | ||
i := i + 1; | i := i + 1; | ||
| Linia 268: | Linia 274: | ||
* <math>N_1 \land i < n \land k = 1 \land l = 0 \land p = 1 \, \implies \, N_2</math> | * <math>N_1 \land i < n \land k = 1 \land l = 0 \land p = 1 \, \implies \, N_2</math> | ||
* <math>N_2 \land p \geq i \, \implies \, N_1[i \mapsto i{+}1][s \mapsto s {+} 6 \cdot k {+} p {-} l]</math> | * <math>N_2 \land p \geq i \, \implies \, N_1[i \mapsto i{+}1][s \mapsto s {+} 6 {\cdot} k {+} p {-} l]</math>. | ||
Pierwsza z nich jest oczywista, natomiast nie jesteśmy w stanie dowieść drugiej! | Pierwsza z nich jest oczywista, natomiast nie jesteśmy w stanie dowieść drugiej! | ||
| Linia 276: | Linia 282: | ||
<math> | <math> | ||
N_2 \, \equiv \, s = i^3 \land k = (1 + 2 + \ldots l) + p \land 1 \leq p \leq l+1 \leq i | N_2 \, \equiv \, s = i^3 \land k = (1 + 2 + \ldots + l) + p \land 1 \leq p \leq l+1 \leq i | ||
</math> | </math> | ||
i wróćmy do ostatniej z implikacji powyżej. | i wróćmy do ostatniej z implikacji powyżej. Wciąż brakuje nam pewnych informacji! | ||
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 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>. | |||
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: | ||
<math> | <math> | ||
N_2 \, \equiv \, s = i^3 \land i < n \land k = (1 + 2 + \ldots l) + p \land 1 \leq p \leq l+1 \leq i. | N_2 \, \equiv \, s = i^3 \land i < n \land k = (1 + 2 + \ldots + l) + p \land 1 \leq p \leq l+1 \leq i. | ||
</math> | </math> | ||
Teraz dowód ostatniej implikacji jest możliwy. | Teraz dowód ostatniej implikacji jest możliwy. | ||
Zauważmy w szczególności, że warunek <math>p \geq i</math> w połączeniu z warunkiem <math>p \leq l{+}1 \leq i</math> obecnym w <math>N_2</math> | Zauważmy w szczególności, że warunek <math>p \geq i</math> w połączeniu z warunkiem <math>p \leq l{+}1 \leq i</math> obecnym w <math>N_2</math> daje nam <math>p = l{+}1 = i</math>. | ||
daje nam <math>p = l{+}1</math>. | Ponieważ <math>p = l{+}1</math> mamy: | ||
<math> | <math> | ||
s | s + 6 {\cdot} k + p {-} l \, = \, s + 6 {\cdot} (1 + 2 + \ldots + (l{+}1)) + 1 | ||
</math> | </math> | ||
a ponieważ <math> | a ponieważ <math>l{+}1 = i</math>, otrzymujemy: | ||
<math> | <math> | ||
s | s + 6 {\cdot} k + p {-} l \, = \, s + 6 {\cdot} (1 + 2 + \ldots + (l{+}1)) + 1 \, = \, s + 6 {\cdot} (1 + 2 + \ldots + i) + 1 \, = \, s + 6 {\cdot} \frac{i {\cdot} (i+1)}{2} + 1 \, = \, | ||
s + 3 \cdot i^2 + | s + 3 {\cdot} i^2 + 3 {\cdot} i + 1 = (i+1)^3. | ||
</math> | </math> | ||
| Linia 350: | Linia 354: | ||
<math>{\color{Red}\{N' \land l < p\}}</math> | <math>{\color{Red}\{N' \land l < p\}}</math> | ||
<math>{\color{Green}\Downarrow}</math> <span style="color:brown">// 6 </span> | <math>{\color{Green}\Downarrow}</math> <span style="color:brown">// 6 </span> | ||
<math>{\color{Red}\{N_2[p \mapsto 1][l mapsto l{+}1]\}}</math> | <math>{\color{Red}\{N_2[p \mapsto 1][l \mapsto l{+}1]\}}</math> | ||
l := l + 1; | l := l + 1; | ||
p := 1 | p := 1 | ||
| Linia 371: | Linia 375: | ||
* <math>N_2 \land p < i \, \implies \, N'[k \mapsto k{+}1] \land p < i</math> | * <math>N_2 \land p < i \, \implies \, N'[k \mapsto k{+}1] \land p < i</math> | ||
* <math>N' \land l < p < i \, \implies \, N_2[p \mapsto 1][l mapsto l{+}1]</math> | * <math>N' \land l < p < i \, \implies \, N_2[p \mapsto 1][l \mapsto l{+}1]</math> | ||
* <math>N' \land l \geq p < i \, \implies \, N_2[p \mapsto p{+}1]</math>. | * <math>N' \land l \geq p < i \, \implies \, N_2[p \mapsto p{+}1]</math>. | ||
| Linia 383: | Linia 387: | ||
<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ść | 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>. | ||
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>. | ||
| Linia 412: | Linia 416: | ||
<math>{\color{Red}[N_2]}</math> | <math>{\color{Red}[N_2]}</math> | ||
while <math>{\color{Red}[N_2]}</math> p < i do <math>{\color{Red}[\mathbf{decr}\, \langle i {-} l, i {-} p \rangle \,\mathbf{in}\, {\,\mathbb{N}\,}^2 \,\mathbf{wrt}\, <_{\mbox{lex}}]}</math> | while <math>{\color{Red}[N_2]}</math> p < i do <math>{\color{Red}[\mathbf{decr}\, \langle i {-} l, i {-} p \rangle \,\mathbf{in}\, {\,\mathbb{N}\,}^2 \,\mathbf{wrt}\, <_{\mbox{lex}}]}</math> | ||
( | ( | ||
... | ... | ||
) | ) | ||
) | ) | ||
<math>{\color{Red}[N_2 \land p \geq i]}</math> | <math>{\color{Red}[N_2 \land p \geq i]}</math> | ||
<math>{\color{Green}\Downarrow}</math> <span style="color:brown">// 4 </span> | <math>{\color{Green}\Downarrow}</math> <span style="color:brown">// 4 </span> | ||
<math>{\color{Red}[N_1[i \mapsto i{+}1][s \mapsto s {+} 6 \cdot k {+} p {-} l]]}</math> | <math>{\color{Red}[N_1[i \mapsto i{+}1][s \mapsto s {+} 6 {\cdot} k {+} p {-} l]]}</math> | ||
s := s + 6 * k + p - l; | s := s + 6 * k + p - l; | ||
i := i + 1; | i := i + 1; | ||
| Linia 448: | Linia 446: | ||
<math>{\color{Red} | <math>{\color{Red}[(\forall x. 1 \leq x < n \implies A[x] \leq A[x+1]) \land (\forall x. n{+}1 \leq x < 2 {\cdot} n \implies A[x] \leq A[x+1])]}</math> | ||
i := 1; j := 2 * n; | i := 1; j := 2 * n; | ||
while A[i] < A[j] do | while A[i] < A[j] do | ||
| Linia 454: | Linia 452: | ||
i := i + 1; | i := i + 1; | ||
j := j - 1; | j := j - 1; | ||
<math>{\color{Red} | <math>{\color{Red}[\forall x, y. 1 \leq x \leq n < y \leq 2 {\cdot} n \implies A[x] \geq A[y]]}</math> | ||
Wersja z 13:25, 16 sie 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:
z := 1; p := x; q := y;
while q <> 0 do
if odd(q) then
z := z * p;
q := q div 2;
p := p * p
Rozwiązanie
{{{3}}}
Ćwiczenie 2
Przeprowadź dowód poprawności całkowitej poniższego programu.
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;
Wskazówka
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.
i := 1; j := 2 * n; while A[i] < A[j] do ,,zamień A[i] i A[j]"; i := i + 1; j := j - 1;
