### VI.6 Statements

#### Statements [Slide 194]

• Simple statements: skip, empty, more, length, assignments, list statements.
• Compound statements: choice, loop, sequential, parallel, always, sometimes, functions, predicates.

#### Simple [Slide 195]

 empty|more|skip|len(ae)

The len construct can be used to deﬁne any interval length. The term len(n) deﬁnes an interval of length n (containing n+1 states). Thus,

 len(0) = empty len(1) = skip

Example 67.

 A = 0 and empty A = 0 and more A = 0 and skip

#### Assignments [Slide 196]

• simple: a = e, A = e
• unit: (nextA) = e, A := e
• gets: A gets e
• temporal: A < e
• stable: stable(A)

Example 68.

 A = 5 + B A := A + 1 A gets B + 1 A <− B + 1 stable(B)

#### Choice [Slide 197]

 ifbe then st1 else st2|ifbe then st1|be implies st1

The form if then is the same as if then else true and is the same as implies

Example 69.

 ifA > 0 then B := B + 4 else B := B + 2 ifA > 0 then B := A + 4

#### Loop [Slide 198]

 whilebe do st|repeatst untilbe| fora

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 > 0 do A := A − 1 repeatB := B + 1 untilB = 5 fori < n do L[i] := L[i] + 1 chopstar(A := A + 1) l = [0, 1, 2] and fore inl do {skip  and output(e)}

#### Sequential [Slide 199]

 st1;st2

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

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

Example 71.

 {A = 0 and empty} ; {B = 0} {A := A + 1 and skip} ; {B := B + 1}

#### Parallel [Slide 200]

 st1  and st2

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

len(5) and always{I = 0} and always{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 = 0 and B = 1 and A := A + 1 and B := B + 1 and skip {A = 0 and empty} ; {B = 0 and empty} {A := A + 1 and stable(B)} ; {B := B + 1 and stable(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 = 0 and next(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(ifmore then A := 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 = 0 and I gets I + 1 and halt(I = 10) and sometimes{I = 5}

will succeed.

Example 75.

 I = 0 and I gets I + 1 and len(2) and sometimes(I = 5) I = 0 and I gets I + 1 and len(7) and sometimes(I = 2)

#### Halt [Slide 204]

 halt(be)

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

I = 0 and I gets I + 1 and halt(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 = 5 and I gets I + 1 and halt(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) and keep{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 = 0 and stable(J) and I = 0 and I gets I + 1 and len(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 = 0 and J = 1 and … and existsI : {I = J and …} }

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 = 0 and stable(J) and I = 0 and I gets I + 1 and len(3) and ﬁn(J = 0)}

#### Forall [Slide 207]

 foralla

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 and p(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 >= J then I else J}. 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’.

Example 81.

define hanoi(n) = exists L,C,R : {
list(L,n) and forall i<n : L[i]=i and
C=[] and R=[] and move(n,L,C,R) and
always format("L=%10t C=%10t R=%10t\n",L,C,R)
}.
/ Move n discs from peg A to peg B /
define move(n,A,B,C) = {
if n=0 then empty
else {
move(n-1,A,C,B);
{skip and A:=A[1..|A|] and B:=A[0..1]+B and C:=C};
move(n-1,C,B,A)
}
}.

#### Input/Output [Slide 210]

 input(V )|output(e)|format("string",e1,…,en)

The input, output and format constructs are for input and output. The “string” in format is like C.

Example 82.

 existsI,J : {input(I)  andJ = 0  and alwaysoutput(J)  and halt(I = 0)  and (I  gets I − 1)  and (J  gets J + I) }.