Strona główna

logika Hoare'a

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

Ćwiczenia 18: Logika Hoare'a

pon., 12/06/2010 - 02:38 — kubica
  1. 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 \}\]
  2. Udowodnij poprawność programu iteracyjnego obliczającego silnię.
  3. [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;
 
Subskrybuje zawartość