Semantyka i weryfikacja programów/Ćwiczenia 13

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\ge 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{?}{\{\alpha \}x:=e\{\beta \}}$

$\frac{?}{\{\alpha \}\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}b\mathbf{𝐝}\mathbf{𝐨}I\{\beta \}}$

Rozwiązanie

{{{3}}}

Ćwiczenie 3 (potęgowanie binarne)

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

$\{y\ge 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ść $\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐮}\mathbf{𝐞}$ wtedy i tylko wtedy, gdy q jest nieparzyste.

Rozwiązanie

{{{3}}}

Ćwiczenie 4

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

Rozwiązanie

{{{3}}}

}

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

</math>

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

$\frac{\{\beta \}I\{\beta \}}{\{\beta \}\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐩}\mathbf{𝐞}\mathbf{𝐚}\mathbf{𝐭}I\mathbf{𝐮}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐥}b\{\beta \wedge 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{\{\alpha \}I\{\beta \}\beta \wedge \mathrm{\neg }b⟹\alpha }{\{\alpha \}\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐩}\mathbf{𝐞}\mathbf{𝐚}\mathbf{𝐭}I\mathbf{𝐮}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐥}b\{\beta \wedge b\}}$

}}

Zadania domowe

Ćwiczenie 1

Wyprowadź ostatnią regułę dla pętli $\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐩}\mathbf{𝐞}\mathbf{𝐚}\mathbf{𝐭}$ 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\ge 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\le x<b^3\}$

Wskazówka

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