Terminators

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#>.