Teorija Programskih Jezikov (IŠRM)/Stari kolokviji in izpiti/Kolokvij-2005-12-15/3. naloga

Iz MaFiRaWiki

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

\{n >= 0 \land m = n\}
k := 1;
while n > 0 do
n := n - 1;
k := 2 * k
done
{k = 2m}

Dodatna naloga: Dokaži še popolno pravilnost.

/Rešitev

Osebna orodja