Example using loops

INTEGER beneficiary count
INTEGER the number of beneficiary
PERSON the sole beneficiary
PERSON the sole executor

GOAL DOCUMENT Distributing Beneficiary using repeat-until PROVIDES
    IF the number of beneficiary IS GREATER THAN 1 THEN BEGIN
        beneficiary count IS the number of beneficiary
        REPEAT
            NUMBERED PARAGRAPH I give 1/<the number of beneficiary> of my estate to beneficiary <beneficiary count>
            ASSERT beneficiary count IS beneficiary count MINUS 1
        UNTIL beneficiary count IS LESS THAN 1
    END ELSE
        BEGIN
            NUMBERED PARAGRAPH I give the whole of my estate to <the sole beneficiary>
            NUMBERED PARAGRAPH I appoint <the sole executor> as my sole executor.
        END

GOAL DOCUMENT Distributing Beneficiary using while-do PROVIDES
    IF the number of beneficiary IS GREATER THAN 1 THEN BEGIN
        beneficiary count IS the number of beneficiary
        WHILE beneficiary count IS GREATEREQUAL THAN 1
        DO
        BEGIN
            NUMBERED PARAGRAPH I give 1/<the number of beneficiary> of my estate to beneficiary <beneficiary count>
            ASSERT beneficiary count IS beneficiary count MINUS 1
        END        
    END ELSE
        BEGIN
            NUMBERED PARAGRAPH I give the whole of my estate to <the sole beneficiary>
            NUMBERED PARAGRAPH I appoint <the sole executor> as my sole executor.
        END