Semantyka i weryfikacja programów/Ćwiczenia 13: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 19: | Linia 19: | ||
y := y + x; | y := y + x; | ||
x := x + 1 | x := x + 1 | ||
<math>{\color{Red}\{y=\frac{n\cdot(n+1)}{2}\}}</math> | <math>{\color{Red}\{y=\frac{n{\cdot}(n+1)}{2}\}}</math> | ||
| Linia 38: | Linia 38: | ||
x := x + 1 | x := x + 1 | ||
) | ) | ||
<math>{\color{Red}\{y=\frac{n\cdot(n+1)}{2}\}}</math> | <math>{\color{Red}\{y=\frac{n{\cdot}(n+1)}{2}\}}</math> | ||
| Linia 57: | Linia 57: | ||
x := x + 1 | x := x + 1 | ||
) | ) | ||
<math>{\color{Red}\{y=\frac{n\cdot(n+1)}{2}\}}</math> | <math>{\color{Red}\{y=\frac{n{\cdot}(n+1)}{2}\}}</math> | ||
| Linia 64: | Linia 64: | ||
* <math> n \geq 0 \land x = 1 \land y = 0 \, \implies \, N</math> | * <math> n \geq 0 \land x = 1 \land y = 0 \, \implies \, N</math> | ||
* <math>N \land x > n \, \implies \, y=\frac{n\cdot(n+1)}{2}</math> | * <math>N \land x > n \, \implies \, y=\frac{n{\cdot}(n+1)}{2}</math> | ||
oraz prawdziwa jest trójka: | oraz prawdziwa jest trójka: | ||
| Linia 87: | Linia 87: | ||
Formalnie rzecz biorąc, powinniśmy teraz zgadnąć asercję, która może być wpisana pomiędzy dwie instrukcje przypisania: | |||
| Linia 122: | Linia 122: | ||
<math>{\color{Red}\{N \land x \leq n\}}</math> | <math>{\color{Red}\{N \land x \leq n\}}</math> | ||
<math>{\color{Green}\Downarrow}</math> <span style="color:brown">// tę implikację należy udowodnić </span> | <math>{\color{Green}\Downarrow}</math> <span style="color:brown">// tę implikację należy udowodnić </span> | ||
<math>{\color{Red}\{N[x \mapsto x{+}1]\}}</math> | <math>{\color{Red}\{N[x \mapsto x{+}1][y \mapsto y{+}x]\}}</math> | ||
y := y + x; | y := y + x; | ||
<math>{\color{Red}\{N[x \mapsto x{+}1]\}}</math> | <math>{\color{Red}\{N[x \mapsto x{+}1]\}}</math> | ||
| Linia 129: | Linia 129: | ||
Skoro dwie asercje ,,spotkały się", wystarczy teraz udowodnić implikację. | Skoro dwie asercje ,,spotkały się", wystarczy teraz udowodnić implikację. | ||
I tak dalej. To znaczy, podobnie postępujemy z pozostałymi przypisaniami. | I tak dalej. To znaczy, podobnie postępujemy z pozostałymi przypisaniami. A wszędzie, gdzie ,,spotykają się" dwie asercje, dowodzimy implikacji. | ||
A wszędzie, gdzie ,,spotykają się" dwie asercje, dowodzimy implikacji. | |||
Podsumowując, poniższe anotacje całego programu powinny stanowić dowód poprawności częściowej: | Podsumowując, poniższe anotacje całego programu powinny stanowić dowód poprawności częściowej: | ||
| Linia 153: | Linia 152: | ||
<math>{\color{Red}\{N \land x > n\}}</math> | <math>{\color{Red}\{N \land x > n\}}</math> | ||
<math>{\color{Green}\Downarrow}</math> <span style="color:brown">// 3 </span> | <math>{\color{Green}\Downarrow}</math> <span style="color:brown">// 3 </span> | ||
<math>{\color{Red}\{y=\frac{n\cdot(n+1)}{2}\}}</math> | <math>{\color{Red}\{y=\frac{n{\cdot}(n+1)}{2}\}}</math> | ||
| Linia 160: | Linia 159: | ||
# <math>n \geq 0 \land x = 1 \land y = 0 \, \implies \, N</math> | # <math>n \geq 0 \land x = 1 \land y = 0 \, \implies \, N</math> | ||
# <math>N \land x \leq n \, \implies \, N[x \mapsto x{+}1][y \mapsto y{+}x]</math> | # <math>N \land x \leq n \, \implies \, N[x \mapsto x{+}1][y \mapsto y{+}x]</math> | ||
# <math>N \land x > n \, \implies \, y=\frac{n\cdot(n+1)}{2}</math> | # <math>N \land x > n \, \implies \, y=\frac{n{\cdot}(n+1)}{2}</math> | ||
Co ciekawe, to wszystko uczyniliśmy nie wiedząc wogóle, jaki jest niezmiennik pętli! | Co ciekawe, to wszystko uczyniliśmy nie wiedząc wogóle, jaki jest niezmiennik pętli! | ||
| Linia 167: | Linia 166: | ||
Należy oczywiście uwzględnić również implikacje, które wypisaliśmy powyżej. | Należy oczywiście uwzględnić również implikacje, które wypisaliśmy powyżej. | ||
Spróbujmy <math>N \, \equiv \, y = \frac{x\cdot(x{-}1)}{2} \land x \leq n{+}1</math>. | Spróbujmy <math>N \, \equiv \, y = \frac{x{\cdot}(x{-}1)}{2} \land x \leq n{+}1</math>. | ||
Nierówność <math>x \leq n{+}1</math> jest niezbędna. | Nierówność <math>x \leq n{+}1</math> jest niezbędna. Potrzebujemy jej po to, aby z <math>N \land x > n</math> wywnioskować <math>x = n{+}1</math>. | ||
Implikacje są prawdziwe więc niezmiennik został wybrany poprawnie. | Implikacje są prawdziwe więc niezmiennik został wybrany poprawnie. | ||
Zauważmy, że niezmiennik nie zawiera wymagania <math>x \geq 1</math>. | Zauważmy, że niezmiennik nie zawiera wymagania <math>x \geq 1</math>. Moglibyśmy je jednak dodać otrzymując <math>N' \, \equiv \, y = \frac{x{\cdot}(x{-}1)}{2} \land 1 \leq x \leq n{+}1</math>. | ||
Moglibyśmy je jednak dodać otrzymując <math>N' \, \equiv \, y = \frac{x\cdot(x{-}1)}{2} \land 1 \leq x \leq n{+}1</math>. | Wszystkie implikacje pozostają prawdziwe, więc jest to też poprawny wybór. Ponadto wiedząc, że <math>x \geq 1</math> możemy, dla czytelności, zapisywać niezmiennik w meta-notacji: | ||
Wszystkie implikacje pozostają prawdziwe, więc jest to też poprawny wybór. | |||
Ponadto wiedząc, że <math>x \geq 1</math> możemy, dla czytelności, zapisywać niezmiennik w meta-notacji: | |||
<math> | <math> | ||
N \, \equiv \, y = 1{+}\ldots{+}(x{-}1) \land x \leq n{+}1. | N \, \equiv \, y = 1{+}2{+}\ldots{+}(x{-}1) \land x \leq n{+}1. | ||
</math> | </math> | ||
'''Pytanie:''' dlaczego nie potrzebowaliśmy warunku <math>x \geq 0</math>? Jak będzie działał nasz program, jeśli zmienną x zainicjujemy wartością ujemną (zamiast x := 1)? | '''Pytanie:''' dlaczego nie potrzebowaliśmy warunku <math>x \geq 0</math>? Jak będzie działał nasz program, jeśli zmienną x zainicjujemy wartością ujemną (zamiast x := 1), np. x := -2, y := 3? | ||
<br> | <br> | ||
| Linia 188: | Linia 184: | ||
<br> | <br> | ||
Niezmiennik pętli będziemy zwykle wpisywać pomiędzy słowem kluczowym while a dozorem pętli. | Niezmiennik pętli będziemy zwykle wpisywać pomiędzy słowem kluczowym while a dozorem pętli. W naszym przypadku otrzymamy następujące anotacje: | ||
W naszym przypadku otrzymamy następujące anotacje: | |||
| Linia 214: | Linia 209: | ||
<math>{\color{Red}\{n \geq 0 \land x = 1 \land y = 0\}}</math> | <math>{\color{Red}\{n \geq 0 \land x = 1 \land y = 0\}}</math> | ||
pomiędzy początkowe przypisania a pętlę. | pomiędzy początkowe przypisania a pętlę. Mogliśmy uczynić inaczej i wpisać w to miejsce po prostu niezmiennik <math>N</math>. Wtedy należałoby wykazać: | ||
Mogliśmy uczynić inaczej i wpisać w to miejsce po prostu niezmiennik <math>N</math>. | |||
Wtedy należałoby wykazać: | |||
| Linia 258: | Linia 251: | ||
<math>{\color{Red}\{N \land x > n\}}</math> | <math>{\color{Red}\{N \land x > n\}}</math> | ||
<math>{\color{Green}\Downarrow}</math> <span style="color:brown">// 3 </span> | <math>{\color{Green}\Downarrow}</math> <span style="color:brown">// 3 </span> | ||
<math>{\color{Red}\{y=\frac{n\cdot(n+1)}{2}\}}</math> | <math>{\color{Red}\{y=\frac{n{\cdot}(n+1)}{2}\}}</math> | ||
| Linia 289: | Linia 282: | ||
<math> | <math> | ||
\frac{\alpha \, implies \, \beta[x \mapsto e]} | \frac{\alpha \, \implies \, \beta[x \mapsto e]} | ||
{{\color{Red}\{\alpha\}} x:= e {\color{Red}\{\beta\}}} | {{\color{Red}\{\alpha\}} x:= e {\color{Red}\{\beta\}}} | ||
</math> | </math> | ||
| Linia 328: | Linia 321: | ||
<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"> | ||
Jako niezmiennik pętli przyjmijmy <math>N \, \equiv \, z \cdot p^q = x^y</math>. | Jako niezmiennik pętli przyjmijmy <math>N \, \equiv \, z {\cdot} p^q = x^y</math>. Oto odpowiednie anotacje naszego programu: | ||
Oto odpowiednie anotacje naszego programu: | |||
| Linia 342: | Linia 334: | ||
if odd(q) then | if odd(q) then | ||
( | ( | ||
<math>{\color{Red}\{N \land q \neq 0 \land \odd(q)\}}</math> | <math>{\color{Red}\{N \land q \neq 0 \land \,\mathrm{odd}(q)\}}</math> | ||
<math>{\color{Red}\{N[p \mapsto p \cdot p][ | <math>{\color{Red}\{N[p \mapsto p {\cdot} p][q \mapsto q \,\mathrm{div}\, 2][z \mapsto z {\cdot} p]\}}</math> | ||
z := z * p | z := z * p | ||
<math>{\color{Red}\{N[p \mapsto p \cdot p][ | <math>{\color{Red}\{N[p \mapsto p {\cdot} p][q \mapsto q \,\mathrm{div}\, 2]\}}</math> | ||
) | ) | ||
else | else | ||
( | ( | ||
<math>{\color{Red}\{N \land q \neq 0 \land \neq \odd(q)\}}</math> | <math>{\color{Red}\{N \land q \neq 0 \land \neq \,\mathrm{odd}(q)\}}</math> | ||
<math>{\color{Red}\{N[p \mapsto p \cdot p][ | <math>{\color{Red}\{N[p \mapsto p {\cdot} p][q \mapsto q \,\mathrm{div}\, 2]\}}</math> | ||
skip | skip | ||
<math>{\color{Red}\{N[p \mapsto p \cdot p][ | <math>{\color{Red}\{N[p \mapsto p {\cdot} p][q \mapsto q \,\mathrm{div}\, 2]\}}</math> | ||
) | ) | ||
<math>{\color{Red}\{N[p \mapsto p \cdot p][ | <math>{\color{Red}\{N[p \mapsto p {\cdot} p][q \mapsto q \,\mathrm{div}\, 2]\}}</math> | ||
q := q div 2; | q := q div 2; | ||
<math>{\color{Red}\{N[p \mapsto p \cdot p]\}}</math> | <math>{\color{Red}\{N[p \mapsto p {\cdot} p]\}}</math> | ||
p := p * p | p := p * p | ||
<math>{\color{Red}\{N\}}</math> | <math>{\color{Red}\{N\}}</math> | ||
| Linia 368: | Linia 360: | ||
<math>{\color{Red}\{y \geq 0\}}</math> | <math>{\color{Red}\{y \geq 0\}}</math> | ||
<math>{\color{Red}\{1 \cdot x^y = x^y\}}</math> | <math>{\color{Red}\{1 {\cdot} x^y = x^y\}}</math> | ||
z := 1; | z := 1; | ||
p := x; | p := x; | ||
q := y; | q := y; | ||
while <math>{\color{Red}\{z \cdot p^q = x^y\}}</math> q <> 0 do | while <math>{\color{Red}\{z {\cdot} p^q = x^y\}}</math> q <> 0 do | ||
( | ( | ||
<math>{\color{Red}\{z \cdot p^q = x^y \land q \neq 0\}}</math> | <math>{\color{Red}\{z {\cdot} p^q = x^y \land q \neq 0\}}</math> | ||
if odd(q) then | if odd(q) then | ||
( | ( | ||
<math>{\color{Red}\{z \cdot p^q = x^y \land q \neq 0 \land \odd(q)\}}</math> | <math>{\color{Red}\{z {\cdot} p^q = x^y \land q \neq 0 \land \,\mathrm{odd}(q)\}}</math> | ||
<math>{\color{Red}\{(z \cdot p) \cdot (p \cdot p)^(q \div 2) = x^y\}}</math> | <math>{\color{Red}\{(z {\cdot} p) {\cdot} (p {\cdot} p)^{(q \,\mathrm{div}\, 2)} = x^y\}}</math> | ||
z := z * p | z := z * p | ||
<math>{\color{Red}\{z \cdot (p \cdot p)^(q \div 2) = x^y\}}</math> | <math>{\color{Red}\{z {\cdot} (p {\cdot} p)^{(q \,\mathrm{div}\, 2)} = x^y\}}</math> | ||
) | ) | ||
else | else | ||
( | ( | ||
<math>{\color{Red}\{z \cdot p^q = x^y \land q \neq 0 \land \neq \odd(q)\}}</math> | <math>{\color{Red}\{z {\cdot} p^q = x^y \land q \neq 0 \land \neq \,\mathrm{odd}(q)\}}</math> | ||
<math>{\color{Red}\{z \cdot (p \cdot p)^(q \div 2) = x^y\}}</math> | <math>{\color{Red}\{z {\cdot} (p {\cdot} p)^{(q \,\mathrm{div}\, 2)} = x^y\}}</math> | ||
skip | skip | ||
<math>{\color{Red}\{z \cdot (p \cdot p)^(q \div 2) = x^y\}}</math> | <math>{\color{Red}\{z {\cdot} (p {\cdot} p)^{(q \,\mathrm{div}\, 2)} = x^y\}}</math> | ||
) | ) | ||
<math>{\color{Red}\{z \cdot (p \cdot p)^(q \div 2) = x^y\}}</math> | <math>{\color{Red}\{z {\cdot} (p {\cdot} p)^{(q \,\mathrm{div}\, 2)} = x^y\}}</math> | ||
q := q div 2; | q := q div 2; | ||
<math>{\color{Red}\{z \cdot (p \cdot p)^q = x^y\}}</math> | <math>{\color{Red}\{z {\cdot} (p {\cdot} p)^q = x^y\}}</math> | ||
p := p * p | p := p * p | ||
<math>{\color{Red}\{z \cdot p^q = x^y\}}</math> | <math>{\color{Red}\{z {\cdot} p^q = x^y\}}</math> | ||
) | ) | ||
<math>{\color{Red}\{z \cdot p^q = x^y \land q=0\}}</math> | <math>{\color{Red}\{z {\cdot} p^q = x^y \land q=0\}}</math> | ||
<math>{\color{Red}\{z = x^y\}}</math> | <math>{\color{Red}\{z = x^y\}}</math> | ||
| Linia 401: | Linia 393: | ||
Teraz pozostaje tylko pokazać następujące implikacje: | Teraz pozostaje tylko pokazać następujące implikacje: | ||
* <math>y \geq 0 \, \implies \, 1 \cdot x^y = x^y</math> | * <math>y \geq 0 \, \implies \, 1 {\cdot} x^y = x^y</math> | ||
* <math>z \cdot p^q = x^y \land q \neq 0 \land \odd(q) \, \implies \, (z \cdot p) \cdot (p \cdot p)^(q \div 2) = x^y</math> | * <math>z {\cdot} p^q = x^y \land q \neq 0 \land \,\mathrm{odd}(q) \, \implies \, (z {\cdot} p) {\cdot} (p {\cdot} p)^{(q \,\mathrm{div}\, 2)} = x^y</math> | ||
* <math>z \cdot p^q = x^y \land q \neq 0 \land \neq \odd(q) \, \implies \, z \cdot (p \cdot p)^(q \div 2) = x^y</math> | * <math>z {\cdot} p^q = x^y \land q \neq 0 \land \neq \,\mathrm{odd}(q) \, \implies \, z {\cdot} (p {\cdot} p)^{(q \,\mathrm{div}\, 2)} = x^y</math> | ||
* <math>z \cdot p^q = x^y \land q=0 \, \implies \, z = x^y</math> | * <math>z {\cdot} p^q = x^y \land q=0 \, \implies \, z = x^y</math> | ||
Zauważmy, że w niezmienniku nie wymagamy aby <math>q \geq 0</math>, ponieważ nie jest to potrzebne do udowodnienia powyższych implikacji. | Zauważmy, że w niezmienniku nie wymagamy aby <math>q \geq 0</math>, ponieważ nie jest to potrzebne do udowodnienia powyższych implikacji. | ||
Musimy tylko umówić się, na wszelki wypadek, jak działa operacja div, gdy jej argument jest ujemny. | Musimy tylko umówić się, na wszelki wypadek, jak działa operacja div, gdy jej argument jest ujemny. | ||
Przyjmijmy, że <math>q \div 2 = m</math> wtedy i tylko wtedy gdy największą liczbą parzystą nie większą od <math>q</math> jest | Przyjmijmy, że <math>q \,\mathrm{div}\, 2 = m</math> wtedy i tylko wtedy gdy największą liczbą parzystą nie większą od <math>q</math> jest | ||
<math>2 \cdot m</math>. | <math>2 {\cdot} m</math>. | ||
{{uwaga||| | {{uwaga||| | ||
| Linia 417: | Linia 409: | ||
}} | }} | ||
'''Pytanie:''' | '''Pytanie:''' czy niezmiennik pętli jest napewno prawdziwy gdy zmienna q ma wartość ujemną? | ||
</div></div> | </div></div> | ||
| Linia 425: | Linia 417: | ||
{{cwiczenie|4|cw4| | {{cwiczenie|4|cw4| | ||
Zaproponuj | Zaproponuj regułę dla instrukcji <math>\mathbf{repeat}\, I \,\mathbf{until}\, b</math>. | ||
}} | }} | ||
| Linia 444: | Linia 436: | ||
Dwukrotnie odwołujemy się do poprawności częściowej instrukcji <math>I</math>, względem różnych asercji początkowych. | Dwukrotnie odwołujemy się do poprawności częściowej instrukcji <math>I</math>, względem różnych asercji początkowych. | ||
Gdybyśmy chcieli tego uniknąć, moglibyśmy rozważyć <math>\alpha = \beta</math>, | Gdybyśmy chcieli tego uniknąć, moglibyśmy rozważyć <math>\alpha = \beta</math>, otrzymując regułę: | ||
<math> | <math> | ||
| Linia 453: | Linia 445: | ||
</math> | </math> | ||
Jeśli <math>{\color{Red}\{\beta\}} I {\color{Red}\{\beta\}}</math> to <math>{\color{Red}\{\beta \land \neg b\}} I {\color{Red}\{\beta\}}</math>. | Jeśli <math>{\color{Red}\{\beta\}} I {\color{Red}\{\beta\}}</math> to <math>{\color{Red}\{\beta \land \neg b\}} I {\color{Red}\{\beta\}}</math>. Zatem powyzszą regułę można uprościć: | ||
Zatem powyzszą regułę można uprościć: | |||
<math> | <math> | ||
| Linia 510: | Linia 501: | ||
{{wskazowka||| | {{wskazowka||| | ||
<math> | <math> | ||
(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> | ||
}} | }} | ||
Wersja z 13:23, 16 sie 2006
Zawartość
Poprawność częściowa prostych programów w języku Tiny.
Poprawność częściowa
Ćwiczenie 1
Przeprowadź dowód poprawności częściowej poniższego programu:
x := 1; y := 0; while x <= n do y := y + x; x := x + 1
Rozwiązanie
{{{3}}}
Ćwiczenie 2
Uzupełnij poniższe reguły:
Rozwiązanie
{{{3}}}
Ćwiczenie 3 (potęgowanie binarne)
Dowiedź poprawności częściowej poniższego programu:
z := 1; p := x; q := y;
while q <> 0 do
if odd(q) then
z := z * p;
q := q div 2;
p := p * p
Wyrażenie odd(q) ma wartość wtedy i tylko wtedy, gdy q jest nieparzyste.
Rozwiązanie
{{{3}}}
Ćwiczenie 4
Zaproponuj regułę dla instrukcji .
Rozwiązanie
{{{3}}}
Zadania domowe
Ćwiczenie 1
Wyprowadź ostatnią regułę dla pętli z pierwszej reguły.
Ćwiczenie 2
Napisz program obliczający najmniejszy wspólny dzielnik dwóch liczb i przeprowadź dowód poprawności częściowej.
Ćwiczenie 3
Przeprowadź dowód poprawności częściowej:
a = 1; b := 1; y := 1; while y <= x do y := y + 3*a + 3*b + 1; a = a + 2*b + 1; b := b + 1;
Wskazówka
