Oxygene

Helyesség



A nyelv a két féle helyességbizonyítási eszközt támogat:

Ha a valamelyik sérül akkor egy "assertion" lép fel. (Az "assert" egy speciális megszakítás, amit a program tesztelésénél és a hibák javításánál alkalmaznak. Ahhoz, hogy működjenek ezek a megszakítások speciális beállításokkal kell futattni a programot. )

Elő és utófelételek

Az előfeltételt a "require" kulcssó után kell megadni. Az itt felsorolt feltételeknek igaznak kell lennie a metódusba való belépéskor. Például itt megkötéseket tehetünk a metódus paramétereire. Az utófeltételnél megadott feltételek azelőtt értékelődnek ki, mielőtt a metódus befejezőne és a vezérlés az őt hívó blokkba térne vissza. Ezeket a kikőtéseket az "ensure" kulcsó után tehetjük meg. Az elő és utófeltételeket egy osztály metódusánál lehet alkalmazni.

method MyObject.DoWork(aValue); require Assigned(fMyWorker); fMyValue > 0; aValue > 0; begin //… do the work here ensure Assigned(fMyResult); fMyResult.Value >= 5; end;

Invariánsok

Az invriánsnak megfelelő feltételeket az "invariants" szó után lehet megadni. Ezeknek a kikötéseknek mindig igaznak kell lenniük. Az invaránsak két féle változata van. Ez egyik a "public invariants", ami az össze publikus metódus végén le lesz ellenőrizve (az utófeltétel után). A másik válzozat a "private invariants", ami az összes metódus végén (publikus vagy privát) le lesz ellenőrizve.

type MyClass = class; public … some methods or properties public invariants fField1 > 35; SomeProperty = 0; SomeBoolMethod() and not (fField2 = 5); private invariants fField > 0; end;