Elő- és utófeltételek
Az elő- és utófeltételek a rutindefiníciók részei. Használatuk nem kötelező. Ha szerepelnek a rutinban, akkor automatikusan ellenőrzésre kerülnek futási időben és hiba lép fel, ha a feltétel nem igaz.
Az előfeltételt a rutin törzs kezdetéhez kell írni (a változó deklaráció elé). A rutin minden meghívásakor kiértékelődik az előfeltétel, és csak akkor fut le a rutin törzsében lévő kód, ha feltétel igaz.
Az utófeltételek a rutin törzsének végére kerülnek és a rutinból való kilépéskor ellenőrződnek.
Az elő- és utófeltételek egy feltételt és/vagy egy megjegyzést tartalmaznak. Többszörös feltételt a logikai ést jelentő and-el lehet létrehozni. A megjegyzéseknek nincs hatásuk a program futására (azaz nem jelent hibát, ha megjegyzés hamis).
Példa:
func (n:Integer,m:Integer)->(res:Integer) is
pre
n>=0 and m>=1
var
x:Integer
do
...
post
res<> nil
end func
printName is
do
...
post
== a nev a kepernyore lesz nyomtatva
end printName
Mind az elő- és utófeltétel része a rutin interface-ének. A rutin újradefiniálásakor ezeket a feltételeket csak a következő módon lehet megváltoztatni: az előfeltétel csak gyengíthető, az utófeltétel csak szigorítható. Ha az újradefiniált rutinban nincs elő- és utófeltétel, akkor a szülő rutin feltételei érvényesek. Ha az előfeltétel felül lett definiálva, akkor a futási időben tesztelt feltétel a következő: a szülő előfeltétele és az előfeltétel vagyolva, utófeltétel esetén a szülő utófeltétele éselve van az utófeltétellel. Így biztosított, hogy a felüldefiniált rutin legalább azt garantálja, mint a szülője.
Két speciális kifejezés érhető el a feltételekben: az => (implikáció) és az old szó.
Példa:
post
found => index>0
Az old kifejezés csak az utófeltételben érhető el. A rutinból való kilépéskor ezzel lehet ellenőrizni, hogy egy kifejezés értéke változott-e a rutinban.
A következő példában a num globális változó nem változhat meg a rutinban:
Példa:
doSomething(n:Integer) is
pre
n<>nil
...
post
num=old num
end doSomething
Osztályinvariáns
Az osztályinvariánst is meg lehet adni az osztályok denfiniálásakor. Ez a definícíó végére tett [invariant feltétel] záradékkal érhető el. Az invariáns futási időben kerül tesztelésre, minden külső interface rutin hívása előtt és után, valamint a létrehozó rutin futtatása után. Futásidejű hiba keletkezik, ha az osztályinvaráns értéke hamis lesz.