Szintaxis
exception Bankrupt
OverInvested
def invest (amount : int, twice: out int) requires (amount > 0) ensures (twice > amount) raises Bankrupt
twice = 2 * amount
assert (twice > 0)
print "$%s is a lot of money to invest!", amount
raise Bankrupt.OverInvested
A következő nyelvi elemek elérhetők alprogram szinten:
- 'assert': feltétel kiértékelés, mint C
- 'requires': előfeltétel
- 'ensures': utófeltétel
- 'raises': dobható kivétel jelölése (kötelező!)
Ellenőrzés
Az ellenőrzések futásidőben történnek, de ez fordításkor kikpcsolható.