A terminator serves to terminate a refinement or a procedure.
(315,080) (000,070)terminator (000,050)(1,0)030040LEAVE (1,0)030080algorithm-name (1,0)050 (185,040)(20,20)[r] (185,030)(-1,0)160 (025,020)(20,20)[l] (025,010)(1,0)005040WITH (1,0)030100compact-primary (1,0)005 (205,020)(20,20)[rb] (215,020)(0,1)020 (225,040)(20,20)[lt]
The algorithm-name must either be the name of the directly surrounding procedure or of some visible refinement, of whose execution the terminator forms part. If a with-part is given, the algorithm named is left yielding the value of the compact-primary, otherwise it is left yielding no value, and has the (hypothetical) type VOID.