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łę dla instrukcji $\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐩}\mathbf{𝐞}\mathbf{𝐚}\mathbf{𝐭}I\mathbf{𝐮}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐥}b$.

Rozwiązanie

{{{3}}}

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 największy 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$