6.3 Loop Statements

Section 12.2 of the JML Reference Manual describes the annotations that can be associated with a loop in JML, namely loop invariants and loop variants. In BML, loop specifications are stored separately from the program code, with an index to the program counter of the entry point of the loop. If there are several loop specifications associated with a single program counter, the first loop specification is supposed to be specifying the outer loop, the second the first inner loop etc. Basically, the semantics for the loop specification in BML is the same as the one in JML. However, at bytecode level, loops are not explicit in the program text, and the verification procedure needs to handle this appropriately.

Loop invariants are evaluated as program annotations of the program point that the index refers to.

Loop variants describe a relation between the entry states of two iterations of the loop: the variant expression should strictly decrease with each loop iteration. In addition, it should be wellfounded, and this guarantees termination of the loop.

Notice that loop variants can be transformed into a sequence of assert and set annotations, after introducing appropriate ghost variables. This transformation basically proceeds as follows. Let variant be the expression declared in the loop variant clause. We declare ghost variables loop_init (initially set to true) and loop_variant (the preliminary initialisation of which is not essential). If l is the program point where we enter the loop, then at that point we add an assertion

     // assert !loop_init ==> (0 <= variant && variant < loop_variant);

followed by:

     // set loop_init = false;
     // set loop_variant = variant;

This ensures that every time the loop entry point l is reached again, the decrease of the loop variant is checked. Only a path that goes through the loop can set loop_init to false.