A <#4003#>terminator<#4003#> serves to terminate a <#4004#>refinement<#4004#> or a procedure.
(315,080)<#4645#>
(000,070)<#4545#>terminator<#4545#>
206
(000,050)<#4546#>(1,0)<#4006#>030<#4006#> <#5556#>(040,010)<#5559#>LEAVE<#5559#><#5556#> (040,010)
(1,0)<#4009#>030<#4009#><#5561#>#tex2html_wrap7443#(080,010)<#5562#>algorithm-name<#5562#><#5561#>
(1,0)<#4012#>050<#4012#><#4546#>
207
(185,040)<#4013#>(20,20)[r]<#4013#>
(185,030)<#4547#>(-1,0)<#4014#>160<#4014#><#4547#>
(025,020)<#4015#>(20,20)[l]<#4015#>
208
(025,010)<#4548#>(1,0)<#4016#>005<#4016#> <#5568#>(040,010)<#5571#>WITH<#5571#><#5568#> (040,010)
(1,0)<#4019#>030<#4019#><#5573#>#tex2html_wrap7453#(100,010)<#5574#>compact-primary<#5574#><#5573#>
(1,0)<#4022#>005<#4022#><#4548#>
209
(205,020)<#4023#>(20,20)[rb]<#4023#>
(215,020)<#4549#>(0,1)<#4024#>020<#4024#><#4549#>
(225,040)<#4025#>(20,20)[lt]<#4025#>
210
<#4645#>
The <#4026#>algorithm-name<#4026#> must either be the name of the directly surrounding
procedure or of some visible <#4027#>refinement<#4027#>, of whose execution the
<#4028#>terminator<#4028#> forms part. If a with-part is given, the algorithm
named is left yielding the value of the <#4029#>compact-primary<#4029#>, otherwise
it is left yielding no value, and has the (hypothetical) type
<#4030#>VOID<#4030#>.