Elan has a special mechanism for terminating the execution of a particular refinement, which looks like
This mechanism can in particular be used to terminate repetitions
from the inside.
Although it looks much like the infamous goto-statement, the
leave-statement is very different: It does not allow arbitrary
continuation of program execution at some other part of the program
with all its known dangers, but completes the execution of an
algorithm. For this reason, you may name in a leave-statement
only a refinement of whose execution the execution of the leave-statement
is part.
It is even possible to leave a refinement with a value, by
This causes the refinement with that name to be left, yielding
the value of the expression.