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 |
if be then st1 else st2 |if be then st1 |be implies st1 |
The form if … then … is the same as if … then … else true and is the same as … implies …
while be do st |repeat st until be | |
for a <ae do st |chopstar(st) | |
for a in le do st |for a in se do st |for ae 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.
while A > 0 do A := A − 1 |
repeat B := B + 1until B = 5 |
for i < n do L[i] := L[i] + 1 |
chopstar(A := A + 1) |
l = [0,1,2] and for e in l do {skip and output(e)} |
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.
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.
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 st |
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 st |
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 st |
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.
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(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.
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.
exists A : st |exists a : 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
exists I,J : {I = 0 and J = 1 and … and |
exists I : {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.
forall a <ae : st |
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).
define F(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’.
define P(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’.
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(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.
existsI,J : {input(I) andJ = 0 and |
always output(J) and halt(I = 0) and |
(I gets I − 1) and (J gets J + I) |
}. |
load "file". |run st. |
The load command is used to load a file containing a program. The run command is used to run a program.