Previous: Loop Statements, Up: Annotation (of) Statements
In contrast to their JML counterpart, BML debug annotations can contain expressions only. These can be constructed using variables, ghost variables and calls to pure methods as all BML expressions. Debug annotations have no meaning for static verification. At runtime, a BML-aware environment is supposed to print out the values of these debug expressions.