logika Hoare'a

Processing math: 100%

warning: Creating default object from empty value in /usr/share/drupal6/modules/taxonomy/taxonomy.pages.inc on line 33.

Wykład 08: Częściowa poprawność

wt., 12/13/2011 - 00:17 — pch

pon., 12/06/2010 - 02:38 — kubica

Udowodnij następującą trójkę:
$\{ x = x_0,\ y = y_0 \} \mathtt{ y := !x - !y; x := !x - !y; y := !x + !y } \{ x = y_0,\ y = x_0 \}$
Udowodnij poprawność programu iteracyjnego obliczającego silnię.

[PCh]
Określ dla każdego

$n$ , co jest wynikiem funkcji coto i udowodnij to.

 
      x := 0;
      y := 1;
      while !y <= n do 
        x := !x - !y;
        y := !y - !x
      done;