Strona główna › Wstęp do programowania - podejście funkcyjne › Ćwiczenia

Ć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;
 
  4. Dana jest n-elementowa tablica a, w której znajdują się permutacja zbioru \(\{0, 1, \dots n-1\}\).
    Na tablicy wolno wykonywać tylko następujące operacje:

    • length a -- badać wielkość tabicy n,
    • \(a.(i)\) -- odczytywać elementy tablicy, oraz
    • \(\mathtt{zamien}(i,j)\) -- zamieniać elementy wartościami.

    Napisz procedurę zamiany : int array → unit, która posortuje daną tablicę
    (tj. przekształci ją w permutację identycznościową) wykonując minimalną możliwą liczbę zamian.
    Podaj niezmienniki pętli oraz odpowiednie funkcje miary.
    Nie muszą one mieć postaci formuł, ale muszą być ściśle określone.
    Udowodnij pełną poprawność programu.

  5. Podaj niezmiennik pętli i wykaż poprawność następującego programu:
    \( \{ x = x_0 \ge 0 \} \)

    i := 0;
d := 1;
s := 1;
while !s <= !x do
    d := !d + 2;
    s := !s + !d;
    i := !i + 1 
done;

    \(\{ !i = \lfloor{\sqrt{!x_0}}\rfloor \}\)