3.5. Loop clauses

Example 1:

INT fac := 1;
FOR i FROM n BY -1 TO 1
DO fac *:= i OD .

INT a, b; read ((a, b)) PR ASSERT a >= 0 & b > 0 PR;
INT q := 0, r := a;
WHILE r >= b PR ASSERT a = b * q + r & 0 <= r PR
DO (q +:= 1, r -:= b) OD
  PR ASSERT a = b * q + r & 0 <= r & r < b PR

The controlled identifier, e.g., i in Example 1, is defined over the repeating-part. Definitions introduced in the while-part are also valid over the do-part.

If the controlled identifier is not applied in the repeating-part, then the for-part may be omitted. A from-part FROM 1 may be omitted; similarly, BY 1 may be omitted. The to-part may be omitted if no test on the final value of the control-integer is required. A while-part WHILE TRUE may be omitted. For example,

FOR i FROM 1 BY 1 TO n WHILE TRUE DO print("a") ODmay be written

TO n DO print("a") OD.

The hierarchy of ranges is illustrated by:

}

3.5.1. Syntax

a) strong void NEST1 loop clause{5D ,551a} : NEST1 STYLE for part defining new integral TAG2{b}, NEST1 STYLE intervals{c}, NEST1 STYLE repeating part with integral TAG2{e}.

b) NEST1 STYLE for part defining new integral TAG2{a} : STYLE for{94g ,-} token, integral NEST1 new integral TAG2 defining identifier with TAG2{48a } ; where (TAG2) is (letter aleph), EMPTY.

c) NEST1 STYLE intervals{a} : NEST1 STYLE from part{d} option, NEST1 STYLE by part{d} option, NEST1 STYLE to part{d} option.

d) NEST1 STYLE FROBYT part{c} : STYLE FROBYT{94g ,-} token, meek integral NEST1 unit{32d } .

e) NEST1 STYLE repeating part with DEC2{a} : NEST1 new DEC2 STYLE while do part{f}; NEST1 new DEC2 STYLE do part{h}.

f) NEST2 STYLE while do part{e} : NEST2 STYLE while part defining LAYER3{g}, NEST2 LAYER3 STYLE do part{h}.

g) NEST2 STYLE while part defining LAYER3{f} : STYLE while{94g ,-} token, boolean NEST2 enquiry clause defining LAYER3{34c ,-}.

h) NEST3 STYLE do part{e,f} : STYLE do{94g ,-} token, strong void NEST3 serial clause defining LAYER4{32a } , STYLE od{94g ,-} token. {Examples:

}

a)

FOR i WHILE i < n DO task1 OD ·TO n DO task1; task2 OD

b)

FOR i

c)

FROM -5 TO +5

d)

FROM -5

e)

WHILE i < n DO task1 OD ·DO task1; task2 OD

f)

WHILE i < n DO task 1; task2 OD

g)

WHILE i < n

h)

DO task1; task2 OD

3.5.2. Semantics

· let f be the yield of the constituent from-part, if any, of C, and be 1 otherwise;

· let b be the yield of the constituent by-part, if any, of C, and be 1 otherwise;

· let t be the yield of the constituent to-part, if any, of C, and be absent otherwise;

· let E2 be the environ established {nonlocally {3.2.2.b } } around E1, according to the for-part-defining-new-integral-TAG2 of C, and with the integer f;

If t is not absent,

then If b > 0 and i > t or if b < 0 and i < t, then C in E1 {is completed and} yields empty; {

otherwise, Step 3 is taken; }

· E3 is E2;

· w is true;

· E3 is established {perhaps nonlocally {3.2.2.b } } around E2 according to the enquiry-clause of P;

· w is the yield in E3 of that enquiry-clause;

· the constituent do-part of C is elaborated in E3;

· 'integral TAG2' is made to access i + b inside the locale of E2;

· Step 2 is taken again; otherwise,

· C in E1 {is completed and} yields empty. {The loop-clause

FOR i FROM u1 BY u2 TO u3 WHILE condition DO action OD

BEGIN INT f:= u1, INT b = u2, t = u3;
    step2:
      IF (b > 0 & f <= t) OR
         (b < 0 & f >= t) OR b = 0
      THEN INT i = f;
          IF condition
          THEN action; f +:= b; GO TO step2
          FI
      FI
END

begin int f:=u1, int b=u2, t=u3;
   step2:
      if b > 0 ∧ f ≤ t ∨ b < 0 ∧ f ≥ t ∨ b = 0
      then int i = f;
         if condition
         then action; f +:= b; go to step2
         fi
      fi
end

.