DBC - nástroj jass
jass je preprocesor javového zdrojového textu. Umožňuje ve
zdrojovém textu programu vyznačit podmínky, jejichž splnění je za běhu
kontrolováno.
Podmínkami se rozumí:
-
pre- a postconditions u metod (vstupní a výstupní podmínky
metod)
-
invarianty objektů - podmínky, které zůstávají pro objekt v
platnosti mezi jednotlivými operacemi nad objektem
