Semantyka i weryfikacja programów/Ćwiczenia 15

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:

$[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]$

Rozwiązanie

{{{3}}}

Ćwiczenie 2

Przeprowadź dowód poprawności całkowitej poniższego programu.

$\{n\ge 0\}$

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;
 
$\{s=n^3\}$

Wskazówka

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

${\mathrm{\Sigma }}_{j=1}^{m}j=\frac{m\cdot (m+1)}{2}$

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.

$[(\mathrm{\forall }x.1\le x<n⟹A[x]\le A[x+1])\wedge (\mathrm{\forall }x.n+1\le x<2\cdot n⟹A[x]\le A[x+1])]$
i := 1; j := 2 * n;
while A[i] < A[j] do
  ,,zamień A[i] i A[j]";
  i := i + 1;
  j := j - 1;
$[\mathrm{\forall }x,y.1\le x\le n<y\le 2\cdot n⟹A[x]\ge A[y]]$