> O této funkci můžeme ale prohlásit i to, že nezapisuje nikam jinam, než do svých lokálních proměnných, nezneužívá žádný exploit, nemá tendenci k vyvolání výjimky (v úvahu připadá vyčerpání volné paměti)
Tohle mi zavání něčím, co dělá jazyk SPARK sám od sebe.
