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]

The len construct can be used to define any interval length. The term len(n) defines an interval of length n (containing n+1 states). Thus,

Assignments [Slide 196]

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

Choice [Slide 197]

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

Loop [Slide 198]

The while, repeat, chopstar and for statements define sequential loops in the usual way.

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

Sequential [Slide 199]

The ; operator stands for sequential composition. The formula before the ; must define 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 satisfied by a unbounded number of behaviours.

Parallel [Slide 200]

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 defines a new interval of length 5 on which I is always 0 and J is always 1.

Next [Slide 201]

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.

Always [Slide 202]

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.

Sometimes [Slide 203]

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.

Halt [Slide 204]

The halt operator defines the termination condition for an interval. For example, the program:

I = 0 and I gets I + 1 and halt(I = 5)

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

Fin [Slide 205]

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

len(5) and keep{I = 0} and fin{I = 1}

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

Exists [Slide 206]

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

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

Forall [Slide 207]

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

forall i < n : {p(i)}

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

Functions [Slide 208]

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

Procedures [Slide 209]

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

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]

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

System commands [Slide 211]

The load command is used to load a file containing a program. The run command is used to run a program.