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:

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

Rozwiązanie

{{{3}}}

Ćwiczenie 2

Uzupełnij poniższe reguły:

${\frac {?}{{\color {Red}\{\alpha \}}x:=e{\color {Red}\{\beta \}}}}$

${\frac {?}{{\color {Red}\{\alpha \}}\mathbf {while} \,b\,\mathbf {do} \,I{\color {Red}\{\beta \}}}}$

Rozwiązanie

{{{3}}}

Ćwiczenie 3 (potęgowanie binarne)

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

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

Wyrażenie odd(q) ma wartość $\mathbf {true}$ wtedy i tylko wtedy, gdy q jest nieparzyste.

Rozwiązanie

{{{3}}}

Ćwiczenie 4

Zaproponuj regułę dla instrukcji $\mathbf {repeat} \,I\,\mathbf {until} \,b$.

Rozwiązanie

{{{3}}}

Zadania domowe

Ćwiczenie 1

Wyprowadź ostatnią regułę dla pętli $\mathbf {repeat} \,$ 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:

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

Wskazówka

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