# Functional Syntax¶

In this section we give a full overview of the CSPM functional syntax. This is divided up into Expressions, which defines what expressions are, Patterns, which defines CSPM’s pattern syntax, and Statements, which defines what statements (which appear in the context of various comprehensions) are. The relative binding strengths of the operators is given in Binding Strength, and the list of reserved words is documented in Reserved Words.

## Expressions¶

Expressions in CSPM evaluate to values. An expression is either a process expression, which is something that uses one of CSP’s process operators, or a non-process expression. In this section we define the syntax of non-process expressions. The syntax of process expressions is defined separately in Defining Processes.

syntax Function Application f(e1, ..., eN)

Applies the function f to the arguments e1, ..., eN. The arguments have to be of the type that the function expects and, further, must satisfy any type constraints imposed by the function.

syntax Binary Boolean Function e1 and e2, e1 or e2
Return type: Bool

Given two expressions e1 and e2 of type Bool, returns either the boolean conjunction or disjunction of the two values.

Both and and or are lazy in their second argument. Thus, False and error("Error") evaluates to False and True or error("Error") evaluates to True.

syntax Unary Boolean Function not e
Return type: Bool

Given an expression of type Bool, returns the negation of the boolean value.

syntax Comparison e1 < e2, e1 <= e2, e1 > e2, e1 >= e2
Return type: Bool

Given two values of type a type t that satisfies Ord, returns a boolean giving the result of comparing the two values using the selected comparison operator. The comparison performed is dictated by the argument type, as follows:

Argument Type Type of Comparison Examples of True Comparisons
Int Standard integer comparison. 1 < 2, 2 < 4.
Char Compares characters according to their integer value. 'a' < 'b', 'f' < 'z'.
<a> Compares the sequences using the list prefix operator. <> < <1>, <1,2> < <1,2,3>, not (<1,2> < <1,3,4>).
{a} Compares the sets using the subset operator. {} < {1,2}, {4,6} < {4,6,7,8}.
(e1, ..., eN) Compares the tuples lexicographically. (1,2) < (2,0), (1,2) < (1,3), not ((1,2) < (1,1)).
(| k => v |) Compares the maps using the submap relation (i.e. m1 is a submap of m2 if m2 has all keys of m1 and the values are related using the appropriate comparison function). (| |) < (| 1 => 2 |), (| 1 => 1 |) < (| 1 => 2 |), not (| 1 => 2 |) < (| 1 => 2 |), (| 1 => 2 |) <= (| 1 => 2 |).
syntax Dot e1.e2

Given two values of type a and type b returns the result of combining them together using the dot operator. The outcome of this operator depends upon the value of e1. If e1 is anything but a data constructor or channel, then the value e1.e2 is formed. For example, given a definition of f as f(x,y) = x.y, f(1, true) evaluates to 1.true, whilst f(STOP, false) evaluates to STOP.false. If e1 is a data constructor or channel then, informally, e1.e2 combines e2 into the partially constructed event or datatype. When doing so, it also checks that e2 is permitted by the data or channel declarations. For example, given the following definitions:

datatype Type = A.{0} | B.Type.{1}


then evaluating A.1 would throw an error, as 1 is not a value permitted by the definition of Type.

More formally, when combining e1 and e2 using ., e1 is examined to find the first incomplete datatype or event. For example, given the above definitions, if e1 is B.A then e2 will not be combined with the B, but instead with the A as this is the first incomplete constructor. Thus, B.A.0 evaluates to B.(A.0), whilst B.A.0.1 evalutes to B.(A.0).1, as the A is already complete.

Warning

Dot is not intended for use as a general functional programming construct; it is primarily intended for use as a data or event constructor, although it is occasionally used more generally in the context of the Prefix operator. Using it as functional programming construct is not supported and may result in various type-checker errors. Instead, tuples and lists should be used.

syntax Equality Comparison e1 == e2, e1 != e2
Return type: Bool

Given two values of a type t that satisfies Eq, returns a boolean giving the result of comparing the values for equality.

syntax If if b then e1 else e2
Parameters: b (Bool) – The branch condition. e1 (a) – The expression to evaluate if b is true. e2 (a) – The expression to evaluate if b is false.

Evaluates b and then evaluates e1 if b is true and otherwise evaluates e2.

syntax Lambda \ ps @ e

Given a comma separated list of pattern of type a1, …, aN and an expression of type b, constructs a function of type (a1, ..., aN) -> b. When the function is evaluated with arguments as, as is matched against the patterns ps and, if it succeeds, e is evaluated in the resulting environment. If it fails, then an error is thrown.

syntax Let let <declaration list> within e

The let definition allows new definitions to be introduced that are usable only in the expression e. When a let expression is evaluated, the declarations are made available for e during evaluation. The return value of a let expression is equal to the return value of e.

The declaration list is formatted exactly as the top-level of a CSPM-file is, but only external, transparent, function, pattern and timed sections declarations are allowed. For example, the following is a valid let expression:

f(xs) =
let
external normal
<y>^ys = tail(xs)
within normal(if ys == <> then STOP else SKIP)

syntax Literal 0.., True/False, 'c', "string"

CSPM allows integer literals to be written in decimal. Boolean literals can are written as true and false. Character literals are enclosed between ' brackets whilst string literals are enclosed between " brackets. Characters can be escaped using the \\ character. Thus, '\'' evaluates to the character ', whilst "\"" evaluates to the string ".

syntax Binary Maths Operation e1 + e2, e1 - e2, e1 * e2, e1 / e2, e1 % e2
Return type: Int

All maths operations take two arguments of type Int and return a value of type Int giving the result of the appropriate function. Note that unlike many programming languages, e1 / e2 returns the quotient (rounding towards negative infinity), whilst e1 % e2 returns the modulus.

syntax Unary Maths Operation -e
Return type: Int

Returns the negation of the expression e, which must be of type Int.

syntax Parenthesis (e)

Brackets an existing expression without altering the type or value of the expression.

syntax Tuple (e1, ..., eN)

Given n expressions of type a1, etc, returns a tuple of type (a1, ..., an).

syntax Variable v

Returns the value of the variable in the current evaluation environment. These must begin with an alphabetic character and are followed by any number of alphanumeric characters or underscores optionally followed by any number of prime characters ('). There is no limit on the length of identifiers and case is significant. Identifiers with a trailing underscore (such as f_) are reserved for machine-generated code. Variables in modules can be accessed using the :: operator. Thus, if M is a module that exports a variable X, then M::X can be used to refer to that particular X.

### Sequences¶

syntax Concat e1^e2

This operator takes two sequences of type <a> and returns their concatenation. Thus, <1,2>^<3,4> == <1,2,3,4>. This takes time proportional to the length of e1.

syntax List <e1, ..., eN>

Given N expressions, each of some common type a, constructs the explicit list where the ith element is ei.

syntax List Comprehension <e1, ..., eN | s1, ..., sN>

For each value generated by the sequence statements, s1 to sN, evaluates e1 to eN, which must all be of some common type a, and adds them to the list in order. Thus, <x, x+1 | x <- <0,2>> == <0, 1, 2, 3>. The variables bound by the statements are available for use by the ei.

syntax Infinite Int List <e..>
Return type: 

Given e, which must be of type Int, constructs the infinite list of all integers greater than or equal to e. Thus, <5..> == <5,6,7,...>.

syntax Infinite Ranged List Comprehension <e.. | s1, ..., sN>
Return type: 

For each value generated by the sequence statements, s1 to sN, evaluates e and creates the infinite list of all integers starting at e. Thus, <1.. | false> == <>, whilst <1.. | true> == <1..>. The variables bound by the statements are available for use by e.

syntax Ranged Int List <e1..e2>
Return type: 

Given e1 and e2 which must both be of type Int, constructs the list of all integers between e1 and e2, inclusive. For example, <5..7> == <5,6,7>.

syntax Ranged List Comprehension <e1..e2 | s1, ..., sN>
Return type: 

For each value generated by the sequence statements, s1 to sN, evaluates e1 and e2, which must be of type Int, and adds them to the list in order. Thus, <x..y | (x,y) <- <(0,1),(1,2)>> == <0, 1, 1, 2>. The variables bound by the statements are available for use by e1 and e2.

syntax List Length #e
Return type: Int

Given a list of type <a>, returns a value of type Int indicating the length of the list. This takes time proportional to the length of the list.

### Sets¶

syntax Set {e1, ..., eN}

Given N elements of some common type a that satisfies Set, constructs the set containing all of the ei. Thus, for each ei, member(ei, {e1, ..., eN}) evaluates to True.

syntax Set Comprehension {e1, ..., eN | s1, ..., sN}

For each value generated by the set statements, s1 to sN, evaluates e1 to eN, which must all be of some common type a that satisfies Set, and adds them to the resulting set. Thus, {x, x+1 | x <- {0,2}} == {0, 1, 2, 3}. The variables bound by the statements are available for use by the ei.

syntax Infinite Int Set {e..}
Return type: {Int}

Given e, which must be of type Int, constructs the infinite set of all integers greater than or equal to e. Thus, {5..} == {5,6,7,...}.

syntax Infinite Ranged List Comprehension {e.. | s1, ..., sN}
Return type: {Int}

For each value generated by the set statements, s1 to sN, evaluates e and creates the infinite set of all integers starting at e. Thus, {1.. | false} == {}, whilst {1.. | true} == {1..}. The variables bound by the statements are available for use by e.

syntax Ranged Set Comprehension {e1..e2 | s1, ..., sN}
Return type: {Int}

For each value generated by the set statements, s1 to sN, evaluates e1 and e2, which must be of type Int, and adds them to the set in order. Thus, {x..y | (x,y) <- {(0,1),(1,2)}} == {0, 1, 2}. The variables bound by the statements are available for use by e1 and e2.

syntax Ranged Int Set {e1..e2}
Return type: {Int}

Given e1 and e2 which must both be of type Int, constructs the set of all integers between e1 and e2, inclusive. For example, {5..7} == {5,6,7}.

### Enumerated Sets¶

syntax Enumerated Set {| e1, ..., eN |}
Parameters: ei (ti =>* b) – The ith value to compute productions of. (Yieldable b) => {b}

Informally, in the case that the e1 to eN are channels, this operator returns the set of all possible events that can be sent along the channels e1 to eN. Formally, it is equivalent to Union({productions(e1), ..., productions(eN)}), i.e. given N expressions that are data constructors or channels (possibly partially completed), constructs the set of all values of type b that are completions of the expressions, providing b satisfies Yieldable.

The most common use of this operator is to specify synchronisation sets. For example, suppose we have the following channel definitions:

channel c : {0..10}.{0..10}.{0..20}
channel d : {0..10}
channel e


and we wanted to put processes P and Q in parallel, synchronising on all events on channels d and e, and events on channel c that start with a 0. This synchronisation alphabet can be written as {| d, e, c.0 |}, as this returns a set consisting of all events that are on channel d, all events on channel e (i.e. just e itself), and those events on channel c that start with a 0.

syntax Enumerated Set Comprehension {| e1, ..., eN | s1, ..., sM |}
Parameters: ei (ti =>* b) – The ith value to compute productions of. (Yieldable b) => {b}

For each value generated by the set statements, s1 to sN, evaluates productions(e1) to productions(eN), which must all be of some common type a that satisfies Set, and adds them to the resulting set. For example, given the following channel definitions:

channel c : {0..2}.{0..3}.{0}
channel e


Then {| c.x.(x+1), e | x <- {0,2} |} evaluates to {e, c.0.1.0, c.2.3.0}.

As with other comprehensions, the variables bound by the statements are available for use by the ei.

## Maps¶

syntax Map (| k1 => v1, ..., kN => vN |)
Parameters: ki (k) – The ith key. vi (v) – The ith value. (| k => v |)

Constructs a map where each key is mapped to the corresponding value. For example, (| |) == emptyMap and (| 9 => 4 |) == mapFromList(<(9, 4)>). If a key appears more than once then the value that the key is mapped to is picked non-deterministically.

Warning

Note that a space must always occur after the initial (| (thus (||) is invalid syntax). This is to ease ambiguity with interleaves and non-deterministic choices that occur after parentheses.

New in version 3.0.

## Patterns¶

CSPM also allows values to be matched against patterns. For example, the following function, which takes an integer, uses pattern matching to specify different behaviour depending upon the argument:

f(0) = True
f(1) = False
f(_) = error("Invalid argument")


Whilst the above could have been written as an if statement, it is much more convenient to write it in the above format. Patterns also bind variables for use in the resulting expression. For example f(<x>^xs) = e) allows the e to refer to the first element of the list as x and the tail of the list as xs.

Each of the allowed patterns is defined as follows.

syntax Concat Pattern p1^p2

Given two patterns, which must be of a common type <a>, matches a sequence where the start of the sequence matches p1 and the end of the sequence matches p2 . This binds any variable bound by p1 or p2.

Warning

Not every concatenation pattern is valid as it is possible to construct ambiguous patterns. For example, the pattern xs^ys is not valid as there is no way of deciding how to decompose the list into two segments.

syntax Dot Pattern p1.p2

Matches any value of the form a.b where a matches p1 and b matches p2. This, together with Variable Pattern allows datatype values and events to be pattern matched. For example, suppose the following declaration is in scope:

datatype X = A.Int.Bool


Then, A.y.True matches any A data-value where the last component is True, and binds y to the integer value. Note that . associates to the right, and thus matching A.0.True to the pattern x.y would bind x to A and 0.True to y.

Warning

Pattern matching on partially constructed events or datatypes is strongly discouraged, and may be disallowed in a future release.

syntax Double Pattern p1 @@ p2

Given two patterns, which must be of a common type a, matches any value that matches both p1 and p2. This binds any variable bound by p1 or p2. For example, 1 @@ 2 matches no values, whilst xs @@ (<y>^ys) matches any non-empty list, and binds xs to the whole list, y to the head of the list and ys to the tails of the list.

syntax List Pattern <p1, ..., pN>

Given N patterns, which must be of a common type a, matches any list where the ith element matches pi. This binds any variable bound by any of the pi.

syntax Literal Pattern 0..., True/False, 'c'..., "x"...

Pattern Literals are written as expression literals are, and match in the obvious way. They do not bind any variable.

syntax Parenthesis Pattern (p)

This matches any value matched by p, and binds exactly the same variables as p.

syntax Set Pattern {} or {p}

The empty-set pattern matches only the empty set (and binds no value), whilst the singleton set pattern matches any value that is a set consisting of a single element that matches p.

syntax Tuple Pattern (p1, ..., pN)

Given N patterns, each of type ai, matches any tuple where the ith element matches pi. This binds any variable bound by any of the pi.

syntax Variable Pattern v

If v is a data constructor or a channel then v matches only the particular data constructor or channel and binds no value. Otherwise, v matches anything any binds v to the value it was matched against. For example:

channel chan : {0..1}

f(chan.x) = x


In the above, chan is recognised as a channel name, and therefore matches only events of the form chan.x. As x is not a data constructor or a channel it matches anything and binds x to the value.

Warning

As a result of the above rules, using short channel names or data constructor names is strongly discouraged. For example, if a script contains a channel definition such as channel x : ..., then any x in the script will only match the channel x, rather than any value.

syntax Wildcard Pattern _

This matches any value, and does not bind any variable.

## Statements¶

In CSPM, there are a number of comprehension constructs that generate new sets or sequences based on existing sequences or sets. For example, the List Comprehension <x+1 | x <- xs> increments every item in the list xs by 1. Statements occur on the right hand side of such comprehensions and, conceptually, generate a sequence of values that can be consumed. The different types of sequences can be described as follows.

syntax Generator Statement p <- e

Given an expression e of type, {a} if this should generate sets and <a> if this generates sequences, and a pattern p of type a, generates all values from e that match the pattern p. Statements to the right of this may use variables bound by p whilst e may refer to variables bound to the left of it.

syntax Predicate Statement e

Selects only those values such that the expression e, which must be of type Bool, evaluates to True. e may refer to variables bound to the left of it.

## Binding Strength¶

The binding strength for the CSPM operators is given below as a list of the operators in descending order of binding strength (i.e. items higher in the list bind tighter). Thus, as [] appears below ;, this means that P = STOP [] STOP ; STOP is parsed as P = STOP [] (STOP ; STOP). Multiple entries on a single level means that the operators have equal binding strength, meaning that brackets may be necessary to disambiguate the meaning. The associativity of the operators is given in brackets.

1. Parenthesis (non-associative), Rename (non-associative)
2. Concat (left-associative)
3. List Length (left-associative)
4. * / % (left-associative)
5. +, - (left-associative)
6. Comparison (non-associative), Equality Comparison (non-associative)
7. not (left-associative)
8. and (left-associative)
9. or (left-associative)
10. : (non-associative)
11. Dot (right-associative)
12. ?, !, \$ (all left-associative)
13. Guarded Expression, Prefix (all right-associative)
14. Sequential Composition (left-associative)
15. Sliding Choice or Timeout (left-associative)
16. Interrupt (left-associative)
17. External Choice (left-associative)
18. Internal Choice (left-associative)
19. Exception, Generalised Parallel, Alphabetised Parallel (all non-associative)
20. Interleave (left-associative)
21. Hide (left-associative)
22. Replicated Operators (non-associative)
23. Double Pattern (non-associative)
24. Let, If (non-associative)

## Reserved Words¶

Certain words are reserved in CSPM, meaning that they cannot be used as identifiers (such as variable names, function names etc). The following is a complete list of the reserved words:

1. and
2. or
3. not
4. if
5. then
6. else
7. let
8. within
9. channel
10. assert
11. datatype
12. subtype
13. external
14. transparent
15. nametype
16. module
17. exports
18. endmodule
19. instance
20. Timed
21. include
22. false
23. true
24. print
25. type