Download Final report

(2) Loop
The loop instruction offers not as many possibilities, but still a precondition may be assured
this way.
…
from
…
until
exit_condition
loop
call_a
…
end
call_b
…
Figure 3-4: The loop instruction, where exit_condition is a Boolean expression.
As Figure 3-4 illustrates, there are two options, where a precondition can be fulfilled.
a) not exit_condition implies call_a’s precondition
b) exit_condition implies call_b’s precondition
The multi-branch instruction (inspect) has not been included, because it contains only a
special condition (e = vi), where e is an expression of type INTEGER or CHARACTER, and
vi a constant of the corresponding type, and therefore appears rather seldom in code.
Neither the check instruction has been considered, since it is an assertion and can be turned
on or off with assertion monitoring. So they do not appear always in the code.
Implication
With the non-strict Boolean operator and then and implies a call’s precondition can hold
as well (see Figure 3-5).
a) c1 implies call_a’s precondition
b) c2 implies call_b’s precondition
…
c1 implies call_a
…
c2 and then call_b
…
Figure 3-5: Keywords for implication
23