Semantyka i weryfikacja programów/Ćwiczenia 13: Różnice pomiędzy wersjami

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

 ${n \geq 1}$ 
x := 1; y := 0;
while x <= n do
  y := y + x;
  x := x + 1
 ${y = \frac{n \cdot (n + 1)}{2}}$

Rozwiązanie

{{{3}}}

Ćwiczenie 2

Uzupełnij poniższe reguły:

$\frac{?}{{α} x : = e {β}}$

$\frac{?}{{α} 𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I {β}}$

Rozwiązanie

{{{3}}}

Ćwiczenie 3 (potęgowanie binarne)

Dowiedź poprawności częściowej poniższego programu:

 ${y \geq 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 = x^{y}}$

Wyrażenie odd(q) ma wartość $𝐭 𝐫 𝐮 𝐞$ wtedy i tylko wtedy, gdy q jest nieparzyste.

Rozwiązanie

{{{3}}}

Ćwiczenie 4

Zaproponuj regułe dla instrukcji $𝐫 𝐞 𝐩 𝐞 𝐚 𝐭 I 𝐮 𝐧 𝐭 𝐢 𝐥 b$ .

Rozwiązanie

{{{3}}}

}

    {{\color{Red}\{\beta\}} \mathbf{repeat}\, I \,\mathbf{until}\, b {\color{Red}\{\beta \land b\}}}

</math>

Jeśli ${β} I {β}$ to ${β \land \neg b} I {β}$ . Zatem powyzszą regułę można uprościć:

$\frac{{β} I {β}}{{β} 𝐫 𝐞 𝐩 𝐞 𝐚 𝐭 I 𝐮 𝐧 𝐭 𝐢 𝐥 b {β \land b}}$

otrzymując regułę prostszą ale słabszą: we wnętrzu pętli nie możemy korzystać z tego, że począwszy od drugiej iteracji nie zachodzi $b$ !

Jeszcze inna możliwość to:

$\frac{{α} I {β} β \land \neg b ⟹ α}{{α} 𝐫 𝐞 𝐩 𝐞 𝐚 𝐭 I 𝐮 𝐧 𝐭 𝐢 𝐥 b {β \land b}}$

}}

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:

 ${x \geq 0}$ 
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;
 ${(b - 1)^{3} \leq x < b^{3}}$

Wskazówka

$(m + 1)^{3} = m^{3} + 3 \cdot m^{2} + 3 \cdot m + 1$

@@ Linia 121: / Linia 121: @@
   <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>
   y := y + x;
@@ Linia 139: / Linia 139: @@
   y := 0;
   <math>{\color{Red}\{n \geq 0 \land x = 1 \land y = 0\}}</math>
-        <math>{\color{Green}Downarrow}</math>        <span style="color:brown">// 1 </span>
+        <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 1 </span>
   <math>{\color{Red}\{N\}}</math>
   while x <= n do
   (
     <math>{\color{Red}\{N \land x \leq n\}}</math>
-          <math>{\color{Green}Downarrow}</math>        <span style="color:brown">// 2 </span>
+          <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 2 </span>
     <math>{\color{Red}\{N[x \mapsto x{+}1][y \mapsto y{+}x]\}}</math>
     y := y + x;
@@ Linia 152: / Linia 152: @@
   )
   <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>
@@ Linia 197: / Linia 197: @@
   y := 0;
   <math>{\color{Red}\{n \geq 0 \land x = 1 \land y = 0\}}</math>
-        <math>{\color{Green}Downarrow}</math>        <span style="color:brown">// 1 </span>
+        <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 1 </span>
   <math>{\color{Red}\{N\}}</math>
   while  <math>{\color{Red}\{N\}}</math>  x <= n do
@@ Linia 229: / Linia 229: @@
   <math>{\color{Red}\{n \geq 1\}}</math>
-        <math>{\color{Green}Downarrow}</math>        <span style="color:brown">// 1 </span>
+        <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 1 </span>
   <math>{\color{Red}\{N[y \mapsto 0][x \mapsto 1]\}}</math>
   x := 1;
@@ Linia 241: / Linia 241: @@
   <math>{\color{Red}\{n \geq 1\}}</math>
-        <math>{\color{Green}Downarrow}</math>        <span style="color:brown">// 1 </span>
+        <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 1 </span>
   <math>{\color{Red}\{N[y \mapsto 0][x \mapsto 1]\}}</math>
   x := 1;
@@ Linia 249: / Linia 249: @@
   (
     <math>{\color{Red}\{N \land x \leq n\}}</math>
-          <math>{\color{Green}Downarrow}</math>        <span style="color:brown">// 2 </span>
+          <math>{\color{Green}\Downarrow}</math>        <span style="color:brown">// 2 </span>
     <math>{\color{Red}\{N[x \mapsto x{+}1][y \mapsto y{+}x]\}}</math>
     y := y + x;
@@ Linia 257: / Linia 257: @@
   )
   <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>
@@ Linia 433: / Linia 433: @@
 <div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
-<math>\mathbf{repeat}\, I \,\mathbf{until}\, b</math> zachowuje się tak samo jak <math>I; while \neg b \,\mathbf{do}\, I</math>.
+<math>\mathbf{repeat}\, I \,\mathbf{until}\, b</math> zachowuje się tak samo jak <math>I; \mathbf{while}\, \neg b \,\mathbf{do}\, I</math>.
 Stąd łatwo otrzymać regułę:
 <math>
-\frac{<math>{\color{Red}\{\alpha\}}</math> I <math>{\color{Red}\{\beta\}}</math>
+\frac{{\color{Red}\{\alpha\}} I {\color{Red}\{\beta\}}
        \quad
-       <math>{\color{Red}\{\beta \land \neg b\}}</math> I <math>{\color{Red}\{\beta\}}</math>}
+       {\color{Red}\{\beta \land \neg b\}} I {\color{Red}\{\beta\}}}
-      {<math>{\color{Red}\{\alpha\}}</math> \mathbf{repeat}\, I \,\mathbf{until}\, b <math>{\color{Red}\{\beta \land b\}}</math>}
+      {{\color{Red}\{\alpha\}} \mathbf{repeat}\, I \,\mathbf{until}\, b {\color{Red}\{\beta \land b\}}}
 </math>
@@ Linia 447: / Linia 447: @@
 <math>
-\frac{<math>{\color{Red}\{\beta\}}</math> I <math>{\color{Red}\{\beta\}}</math>
+\frac{{\color{Red}\{\beta\}} I {\color{Red}\{\beta\}}
        \quad
-       <math>{\color{Red}\{\beta \land \neg b\}}</math> I <math>{\color{Red}\{\beta\}}</math>}
+       {\color{Red}\{\beta \land \neg b\}}</math> I {\color{Red}\{\beta\}}}
-      {<math>{\color{Red}\{\beta\}}</math> \mathbf{repeat}\, I \,\mathbf{until}\, b <math>{\color{Red}\{\beta \land b\}}</math>}
+      {{\color{Red}\{\beta\}} \mathbf{repeat}\, I \,\mathbf{until}\, b {\color{Red}\{\beta \land b\}}}
 </math>
@@ Linia 457: / Linia 457: @@
 <math>
-\frac{<math>{\color{Red}\{\beta\}}</math> I <math>{\color{Red}\{\beta\}}</math>}
+\frac{{\color{Red}\{\beta\}} I {\color{Red}\{\beta\}}}
-      {<math>{\color{Red}\{\beta\}}</math> \mathbf{repeat}\, I \,\mathbf{until}\, b <math>{\color{Red}\{\beta \land b\}}</math>}
+      {{\color{Red}\{\beta\}} \mathbf{repeat}\, I \,\mathbf{until}\, b {\color{Red}\{\beta \land b\}}}
 </math>
@@ Linia 466: / Linia 466: @@
 <math>
-\frac{<math>{\color{Red}\{\alpha\}}</math> I <math>{\color{Red}\{\beta\}}</math>
+\frac{{\color{Red}\{\alpha\}} I {\color{Red}\{\beta\}}
        \quad
        \beta \land \neg b \implies \alpha}
-      {<math>{\color{Red}\{\alpha\}}</math> \mathbf{repeat}\, I \,\mathbf{until}\, b <math>{\color{Red}\{\beta \land b\}}</math>}
+      {{\color{Red}\{\alpha\}} \mathbf{repeat}\, I \,\mathbf{until}\, b {\color{Red}\{\beta \land b\}}}
 </math>

Semantyka i weryfikacja programów/Ćwiczenia 13: Różnice pomiędzy wersjami

Wersja z 08:16, 14 sie 2006

Zawartość

Poprawność częściowa

Zadania domowe

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia