Semantyka i weryfikacja programów/Ćwiczenia 13

Weryfikacja programow

Ćwiczenie 1

$\{n\ge 1\}$
x := 1; y := 0;
$\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}$ x <= n $\mathbf{𝐝}\mathbf{𝐨}$
  y := y + x;
  x := x + 1
Parser nie mógł rozpoznać (błąd składni): {\displaystyle \{\color{Green}y=\Sigma_{z=1}^{n}z}\}}

Rozwiązanie

$\{n\ge 1\}$
x := 1; y := 0;
while $\{y=\frac{x\cdot (x-1)}{2}\wedge x\le n+1\}$ x <= n do
  $\{y=\frac{x\cdot (x-1)}{2}\wedge x\le n+1\wedge x\le n\}$
  y := y + x;
  x := x + 1
  $\{y=\frac{x\cdot (x-1)}{2}\wedge x\le n+1\}$
$\{y=\frac{x\cdot (x-1)}{2}\wedge x\le n+1\wedge x>n\}$
$\{y=\frac{n\cdot (n+1)}{2}\}$

Zadania domowe

Ćwiczenie 1