ae ::= |
z |random |Random ||le||a |next a |A |next A | |
ae1+ae2 |ae1−ae2 |ae1∗ae2 | |
|
ae1 div ae2 |ae1 mod ae2 |ae1 ∗∗ae2 | |
|
if be then ae1 else ae2 |f(e1,…,en) |
random is an integer random number (static within a state). Random is an integer random number (can change within a state).
be ::= |
true |false |a |next a |A |next A | |
be1 or be2 |be1 and be2 |∼be | |
|
empty |more |e1 = e2 |e1 ∼= e2 | |
|
ae1 <ae2 |ae1 <=ae2 |ae1 >ae2 |ae1 >=ae2 | |
|
if be then be1 else be2 |f(e1,…,en) | |
|
exists i <ae :{f(i,e1,…,en)}| |
|
forall i <ae :{f(i,e1,…,en)} |
le ::= |
a |next a |A |next A | |
le1+le2 |le[ae] |[e1,…,en] |le[ae1..ae2] |
|
To access an element of a list, the notation L[i] should be used. Indexing begins at zero. Thus, for example, if L = [1,2,3,4] then L[2] = 3.
Sublist L[i..j] denotes a sublist of L from i to j − 1. For example, list(L,5) and L[1..3] = [1,2] assigns the values 1 and 2 to the second and third elements of the list.
Declaration:
se ::= |
a |next a |A |next A | |
se1+se2 |se[ae] | se[ae1..ae2] | |
|
"s1…sn" |[s1,…,sn] |
String constants are enclosed in double quotes, e.g. "this is a string". Most of the
C escapes may be used. For example \n introduces a newline character,
and \" introduces a double quote. The character \ itself must be escaped as
\\.
Two strings may be appended with the + operator: "abc"+"def"="abcdef".
fe ::= |
$d.d$ |$d.de± d$ |frandom |fRandom |a |next a | |
A |next A |fe1+fe2 |fe1−ae2 |fe1∗fe2 | |
|
fe1 div fe2 |fe1 mod fe2 |fe1 ∗∗fe2 | |
|
fe1∕fe2 |sqrt(fe) |ceil(fe) |floor(fe) |exp(fe) | |
|
log(fe) |log10(fe) |sin(fe) |cos(fe) |tan(fe) | |
|
asin(fe) |acos(fe) |atan(fe) |atan2(fe1,fe2) | |
|
sinh(fe) |cosh(fe) |tanh(fe) |fabs(fe) |itof(ae) | |
|
if be then fe1 else fe2 |f(e1,…,en) |
The function itof returns the float corresponding to an integer. floor and ceil return respectively the largest integer not greater than, smallest integer not less than. frandom is a float random number in [0.0,1.0) (static within a state). fRandom is a float random number in [0.0,1.0) (can change within a state).
ge ::= | lambda(V 1,…,V n) :{e} |
The command define F(Y ) = {Y + 1} to define a function F is the same as the assignment F = lambda(Y ) : {Y + 1}.