© 1996-2019







VI.5 Expressions

Integer Expressions [Slide 187]

ae ::=
z|random|Random||le||a|nexta|A|nextA|
ae1+ae2|ae1ae2|ae1ae2|
ae1 div ae2|ae1 mod ae2|ae1 ∗∗ae2|
ifbe 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).

Example 60.  

1 + nexta
A + nextB
if((nextA) > B) then C + nextB else (nextC) + D

Boolean Expressions [Slide 188]

be ::=
true|false|a|nexta|A|nextA|
be1 or be2|be1 and be2|be|
empty|more|e1 = e2|e1 = e2|
ae1 <ae2|ae1 <=ae2|ae1 >ae2|ae1 >=ae2|
ifbe then be1 else be2|f(e1,,en)|
existsi <ae :{f(i,e1,,en)}|
foralli <ae :{f(i,e1,,en)}

Example 61.  

empty or (nextA > 0)
existsi < |L| : {L[i] > 5}

List Expressions [Slide 189]

le ::=
a|nexta|A|nextA|
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.

Example 62.  

L1 + nextL2
L[2..5] = [L[2],L[3],L[4]]
List(L, 5)

List Expressions [Slide 190]

Declaration:

  • list(L,n): defines L to be a list of fixed size n.
  • List(L,n): defines L to be a list of variable size up to maximum of n.
  • list(L,n) and List(L,n) apply only on the current state.
  • stable(struct(L)) keeps the list structure of L stable over an interval.

Example 63.  

List(L, 5) and stable(struct(L))

String Expressions [Slide 191]

se ::=
a|nexta|A|nextA|
se1+se2|se[ae]|se[ae1..ae2]|
"s1sn"|[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".

Example 64.  

L1 + nextL2
L[2..5] = [L[2],L[3],L[4]]
L = "abc"

Float Expressions [Slide 192]

fe ::=
$d.d$|$d.de ± d$|frandom|fRandom|a|nexta|
A|nextA|fe1+fe2|fe1ae2|fe1fe2|
fe1divfe2|fe1modfe2|fe1 ∗∗fe2|
fe1fe2|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)|
ifbe 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).

Example 65.

A = cos($0.123$)
nextB = exp($0.123e + 10$)

Lambda Expressions [Slide 193]

ge ::=
lambda(V 1,,V n) :{e}

The command defineF(Y ) = {Y + 1} to define a function F is the same as the assignment F = lambda(Y ) : {Y + 1}.

Example 66.

F = lambda(Y,X) : {X + Y }
G = lambda(Y ) : {lambda(X) : {X + Y }}







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