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 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.
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.
Binary Boolean Function e1 and e2, e1 or e2¶| Return type: | |
|---|
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.
Unary Boolean Function not e¶| Return type: | |
|---|
Given an expression of type Bool, returns the negation of the boolean
value.
Comparison e1 < e2, e1 <= e2, e1 > e2, e1 >= e2¶| Return type: | |
|---|
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'. |
|
Compares the sequences using the list prefix operator. | <> < <1>, <1,2> < <1,2,3>, not (<1,2> < <1,3,4>). |
|
Compares the sets using the subset operator. | {} < {1,2}, {4,6} < {4,6,7,8}. |
|
Compares the tuples lexicographically. | (1,2) < (2,0), (1,2) < (1,3), not ((1,2) < (1,1)). |
|
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 |). |
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.
Equality Comparison e1 == e2, e1 != e2¶| Return type: | |
|---|
Given two values of a type t that satisfies Eq, returns
a boolean giving the result of comparing the values for equality.
If if b then e1 else e2¶| Parameters: |
|
|---|
Evaluates b and then evaluates e1 if b is true and otherwise
evaluates e2.
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) -> bas, 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.
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)
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 ".
Binary Maths Operation e1 + e2, e1 - e2, e1 * e2, e1 / e2, e1 % e2¶| Return type: | |
|---|
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.
Unary Maths Operation -e¶| Return type: | |
|---|
Returns the negation of the expression e, which must be of type
Int.
Parenthesis (e)¶Brackets an existing expression without altering the type or value of the expression.
Tuple (e1, ..., eN)¶Given n expressions of type a1, etc, returns a tuple of type
(a1, ..., an).
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.
Concat e1^e2¶This operator takes two sequences of type <a><1,2>^<3,4> == <1,2,3,4>. This takes time
proportional to the length of e1.
List <e1, ..., eN>¶Given N expressions, each of some common type a, constructs the
explicit list where the ith element is ei.
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.
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,...>.
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.
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>.
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.
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.
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.
Infinite Int Set {e..}¶| Return type: | |
|---|
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,...}.
Infinite Ranged List Comprehension {e.. | s1, ..., sN}| Return type: | |
|---|
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.
Ranged Set Comprehension {e1..e2 | s1, ..., sN}¶| Return type: | |
|---|
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.
Enumerated Set {| e1, ..., eN |}¶| Parameters: | ei ( |
|---|---|
| Return type: | |
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.
Enumerated Set Comprehension {| e1, ..., eN | s1, ..., sM |}¶| Parameters: | ei ( |
|---|---|
| Return type: | |
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.
Map (| k1 => v1, ..., kN => vN |)¶| Parameters: |
|
|---|---|
| Return type: | |
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.
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.
Concat Pattern p1^p2¶Given two patterns, which must be of a common type <a>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.
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.
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.
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.
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.
Parenthesis Pattern (p)¶This matches any value matched by p, and binds exactly the same variables
as p.
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.
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.
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.
Wildcard Pattern _¶This matches any value, and does not bind any variable.
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.
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.
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.
Parenthesis (non-associative), Rename (non-associative)Concat (left-associative)List Length (left-associative)* / % (left-associative)+, - (left-associative)Comparison (non-associative), Equality Comparison
(non-associative)not (left-associative)and (left-associative)or (left-associative): (non-associative)Dot (right-associative)?, !, $ (all left-associative)Guarded Expression, Prefix (all right-associative)Sequential Composition (left-associative)Sliding Choice or Timeout (left-associative)Interrupt (left-associative)External Choice (left-associative)Internal Choice (left-associative)Exception, Generalised Parallel, Alphabetised Parallel
(all non-associative)Interleave (left-associative)Hide (left-associative)Double Pattern (non-associative)Let, If (non-associative)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:
andornotifthenelseletwithinchannelassertdatatypesubtypeexternaltransparentnametypemoduleexportsendmoduleinstanceTimedincludefalsetrueprinttype