Leave in loops

The leave keyword is often more useful in terminating a loop. A leave causes control to transfer to the expression immediately following the loop. As loops always return the unique value of Void, you cannot return a value with leave. That is, leave takes no argument.

f() ==
  i := 1
  repeat
    if factorial(i) > 1000 then leave
    i := i + 1
  i
                    Type: Void

This example is a modification of the last example in the previous section. Instead of using return we’ll use leave.

f()
 7
                    Type: PositiveInteger

The loop terminates when factorial(i) gets big enough. The last line of the function evaluates to the corresponding “good” value of i and the function terminates, returning that value.

You can only use leave to terminate the evaluation of one loop. Lets consider a loop within a loop, that is, a loop with a nested loop. First, we initialize two counter variables.

(i,j) := (1,1)
 1
                    Type: PositiveInteger

repeat
  repeat
    if (i + j) > 10 then leave
    j := j + 1
  if (i + j) > 10 then leave
  i := i + 1
                    Type: Void

Nested loops must have multiple leave expressions at the appropriate nesting level. How would you rewrite this so (i + j) > 10 is only evaluated once?

Leave vs => in loop bodies

Compare the following two loops:

i := 1                      i := 1
repeat                      repeat
  i := i + 1                  i := i + 1
  i > 3 => i                  if i > 3 then leave
  output(i)                   output(i)

In the example on the left, the values 2 and 3 for i are displayed but then the “=>” does not allow control to reach the call to output again. The loop will not terminate until you run out of space or interrupt the execution. The variable i will continue to be incremented because the “=>” only means to leave the block, not the loop.

In the example on the right, upon reaching 4, the leave will be executed, and both the block and the loop will terminate. This is one of the reasons why both “=>” and leave are provided. Using a while clase with the “=>” lets you simulate the action of leave.