© 1996-2019







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 define any interval length. The term len(n) defines 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 <ae do st|chopstar(st)|
forainle do st|forainse do st|forae times do st

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.

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 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.

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 defines 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 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.

Example 76.  

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

Fin [Slide 205]

fin(be)

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.

Example 77.  

J = 0 and stable(J) and
I = 0 and I gets I + 1 and len(3) and fin(J = 0)

Exists [Slide 206]

existsA :st|existsa :st|existsV 1,,V n :st

Existential quantification 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 fin(J = 0)}

Forall [Slide 207]

foralla <ae :st

Universal quantification is denoted by the forall operator. Only the bounded form foralli < n : {} is permitted. Semantically, universal quantification 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]

defineF(V 1,,V n) = {e}.

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

Example 80.  

definemax(I,J) = {ifI >= J then I else J}.
A := A + max(C,D)

Procedures [Slide 209]

defineP(V 1,,V n) = {st}.

The define construct is used to define 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)
}.

System commands [Slide 211]

load"file".|runst.

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







2019-05-10
Contact | Home | ITL home | Course | Proofs | Algebra | FL