The form if…then… is the same as if…then…elsetrue and is the
same as …implies…

Example 69.

ifA > 0thenB := B + 4elseB := B + 2

ifA > 0thenB := A + 4

Loop [Slide 198]

whilebedost|repeatstuntilbe|

fora <aedost|chopstar(st)|

forainledost|forainsedost|foraetimesdost

The while, repeat, chopstar and for statements deﬁne sequential
loops in the usual way.

Note that the control variable of a for loop should be static.

Example 70.

whileA > 0doA := A − 1

repeatB := B + 1untilB = 5

fori < ndoL[i] := L[i] + 1

chopstar(A := A + 1)

l = [0, 1, 2]andforeinldo{skipandoutput(e)}

Sequential [Slide 199]

st_{1};st_{2}

The ; operator stands for sequential composition. The formula before
the ; must deﬁne an interval length. For example,

{I = 0andIgetsI + 1};{len(4)andIgetsI + 1} is not executable,
since it is satisﬁed by a unbounded number of behaviours.

Example 71.

{A = 0andempty};{B = 0}

{A := A + 1andskip};{B := B + 1}

Parallel [Slide 200]

st_{1}andst_{2}

The logical conjunction operator and may be used to compose
programs in parallel. For example, the conjunction

len(5)andalways{I = 0}andalways{J = 1}

causes the terms len(5), always{I = 0}, and always{J = 1} to be
executed concurrently. That is, it deﬁnes a new interval of length 5 on
which I is always 0 and J is always 1.

Example 72.

A = 0andB = 1andA := A + 1andB := B + 1andskip

{A = 0andempty};{B = 0andempty}

{A := A + 1andstable(B)};{B := B + 1andstable(A)}

Next [Slide 201]

nextst

The operator next is the operator. The term next… causes
…
to be executed on the next state. There must be a next state.
Thus,

next{I = 1}

means that the variable I has the value 1 on the next state. It fails if
the interval is empty.

Example 73.

next(A = 0)

B = 0andnext(A = B + 1)

Always [Slide 202]

alwaysst

The operator always is the operator. The term always… causes …to
be executed on every state. Thus,

always{I = 1}

means that the variable I always has the value 1.

Example 74.

always(A = 1)

always(A := A + 1)

always(ifmorethenA := A + 1)

Sometimes [Slide 203]

sometimesst

The operator sometimes is operator. The term sometimes… causes
the interpreter to check that … is true at some time in a program.
Thus,

I = 0andIgetsI + 1andhalt(I = 10)andsometimes{I = 5}

will succeed.

Example 75.

I = 0andIgetsI + 1andlen(2)andsometimes(I = 5)

I = 0andIgetsI + 1andlen(7)andsometimes(I = 2)

Halt [Slide 204]

halt(be)

The halt operator deﬁnes the termination condition for an interval. For
example, the program:

I = 0andIgetsI + 1andhalt(I = 5)

deﬁnes an interval on which I is incremented state-by-state until it
equals 5. The interval length must therefore be 5.

Example 76.

I = 5andIgetsI + 1andhalt(I = 5)

Fin [Slide 205]

ﬁn(be)

The term ﬁn… means that … must be true on the last state of the
interval. Thus, the program

len(5)andkeep{I = 0}andﬁn{I = 1}

deﬁnes an interval of length 5 for which I is 1 on the last state, and 0
on every other state.

Example 77.

J = 0andstable(J)and

I = 0andIgetsI + 1andlen(3)andﬁn(J = 0)

Exists [Slide 206]

existsA :st|existsa :st|existsV_{1},…,V_{n}:st

Existential quantiﬁcation is denoted by the exists operator and
semantically, it corresponds to the introduction of local variables. For
example, in the program

existsI,J : {I = 0andJ = 1and…and

existsI : {I = Jand…}

}

there are two instances of the variable I. The outer one has initial value
0, the inner one has initial value 1.

Example 78.

existsI,J : {J = 0andstable(J)and

I = 0andIgetsI + 1and

len(3)andﬁn(J = 0)}

Forall [Slide 207]

foralla <ae:st

Universal quantiﬁcation is denoted by the forall operator. Only
the bounded form foralli < n : {…} is permitted. Semantically,
universal quantiﬁcation corresponds to indexed concurrency. The
program

foralli < n : {p(i)}

is equivalent to p(0)and…andp(n − 1).

Example 79.

foralli < |L| : {L[i] = 0}

foralli < |L| : {L[i] := L[i] + 1}

Functions [Slide 208]

deﬁneF(V_{1},…,V_{n}) = {e}.

The deﬁne construct can be use to deﬁne functions. The parameters of
a function call are passed via ‘call by reference’.

Example 80.

deﬁnemax(I,J) = {ifI >= JthenIelseJ}.

A := A + max(C,D)

Procedures [Slide 209]

deﬁneP(V_{1},…,V_{n}) = {st}.

The deﬁne construct is used to deﬁne procedures. The parameters of a
procedure call are passed via ‘call by reference’.