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 59: | Linia 59: | ||
<math> | <math> | ||
\frac{l \div 2 \geq 0 \land N'(l) \implies b \quad {\color{Red}[l \div 2 \geq 0 \land N'(l)]} I {\color{Red}[N'(l \div 2)]} \quad N'(0) \implies \neg b} | \frac{l \,\mathrm{div}\, 2 \geq 0 \land N'(l) \implies b \quad {\color{Red}[l \,\mathrm{div}\, 2 \geq 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> | ||
| Linia 66: | Linia 66: | ||
<math>{\color{Red}[l \div 2 \geq 0 \land N'(l)]}</math> | <math>{\color{Red}[l \,\mathrm{div}\, 2 \geq 0 \land N'(l)]}</math> | ||
if odd(q) then | if odd(q) then | ||
z := z * p; | z := z * p; | ||
q := q div 2; | q := q div 2; | ||
p := p * p | p := p * p | ||
<math>{\color{Red}[N'(l \div 2)]}</math> | <math>{\color{Red}[N'(l \,\mathrm{div}\, 2)]}</math> | ||
oraz kolejnych dwóch łatwych implikacji: | oraz kolejnych dwóch łatwych implikacji: | ||
* <math>l \div 2 \geq 0 \land N'(l) \, \implies \, q \neq 0</math> | * <math>l \,\mathrm{div}\, 2 \geq 0 \land N'(l) \, \implies \, q \neq 0</math> | ||
* <math>N'(0) \implies q = 0</math>. | * <math>N'(0) \implies q = 0</math>. | ||
Stosując teraz zwykłe reguły ,,przeciągamy" niezmiennik <math>N'(l \div 2)</math> w tył: | Stosując teraz zwykłe reguły ,,przeciągamy" niezmiennik <math>N'(l \,\mathrm{div}\, 2)</math> w tył: | ||
<math>{\color{Red}[l \div 2 \geq 0 \land z \cdot p^q = x^y \land q = l]}</math> | <math>{\color{Red}[l \,\mathrm{div}\, 2 \geq 0 \land z \cdot p^q = x^y \land q = l]}</math> | ||
if odd(q) then | if odd(q) then | ||
( | ( | ||
<math>{\color{Red}[l \div 2 \geq 0 \land z \cdot p^q = x^y \land q = l \land \odd(q)]}</math> | <math>{\color{Red}[l \,\mathrm{div}\, 2 \geq 0 \land z \cdot p^q = x^y \land q = l \land \odd(q)]}</math> | ||
<math>{\color{Green}\Downarrow}</math> | <math>{\color{Green}\Downarrow}</math> | ||
<math>{\color{Red}[(z \cdot p) \cdot (p \cdot p)^(q \div 2) = x^y \land q \div 2 = l \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 \div 2) = x^y \land q \div 2 = l \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 \div 2) = x^y \land q \div 2 = l \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 \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 \div 2]}</math> | <math>{\color{Red}[z \cdot p^q = x^y \land q = l \,\mathrm{div}\, 2]}</math> | ||
| Linia 104: | Linia 104: | ||
... | ... | ||
while <math>{\color{Red}[N]}</math> q <> 0 do <math>{\color{Red}[\mathbf{decr}\, q \,\mathbf{in}\, \ | while <math>{\color{Red}[N]}</math> q <> 0 do <math>{\color{Red}[\mathbf{decr}\, q \,\mathbf{in}\, \,\mathbb{N}\, \,\mathbf{wrt}\, <]}</math> | ||
( | ( | ||
if odd(q) then | if odd(q) then | ||
| Linia 147: | Linia 147: | ||
{{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> | ||
<math> | <math> | ||
| Linia 402: | Linia 402: | ||
s := 1; | s := 1; | ||
i := 1; | i := 1; | ||
while <math>{\color{Red}[N_1]}</math> i < n do <math>{\color{Red}[\mathbf{decr}\, n{-}i \,\mathbf{in}\, \ | while <math>{\color{Red}[N_1]}</math> i < n do <math>{\color{Red}[\mathbf{decr}\, n{-}i \,\mathbf{in}\, \,\mathbb{N}\, \,\mathbf{wrt}\, <]}</math> | ||
( | ( | ||
<math>{\color{Red}[N_1 \land i < n]}</math> | <math>{\color{Red}[N_1 \land i < n]}</math> | ||
| Linia 411: | Linia 411: | ||
<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}[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}\, {\ | 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> | ||
( | (, | ||
... | ... | ||
if l < p then | if l < p then | ||
| Linia 448: | Linia 448: | ||
<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> | <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 454: | ||
i := i + 1; | i := i + 1; | ||
j := j - 1; | j := j - 1; | ||
<math>{\color{Red}\{forall x, y. 1 \leq x \leq n < y \leq 2 \cdot n \implies A[x] \geq A[y]\}}</math> | <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 08:36, 14 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;
