Teorija Programskih Jezikov (IŠRM)/Stari kolokviji in izpiti/Izpit-2007-02-24/2. naloga

Iz MaFiRaWiki

S pravili za dokazovanje pravilnosti dokaži, da velja naslednja delna pravilnost:

  1. {n >= 0}
  2. k := 0
  3. while 2*k + 1 < n do
  4. k := k + 1
  5. done
  6. {k = |n/2|}

Opomba: oznaka | x | pomeni x zaokroženo navzdol, na primer 3.9 = 3.

Dodatna naloga (+10 točk) Dokaži še popolno pravilnost programa.

/Rešitev

Osebna orodja