A.1 Expressions

At a basic level, a CSP_Mscript defines processes, along with supporting functions and expressions. CSP draws freely on mathematics for these supporting terms, so the CSP_Mexpression-language is rich and includes direct support for sequences, sets, booleans, tuples, user-defined types, local definitions, pattern-matching and lambda terms.

We will use the following variables to stand for expressions of various types.

m, n	numbers
s, t	sequences
a, A	sets (the latter a set of sets)
b	boolean
p, q	processes
e	events
c	channel
x	general expression

When writing out equivalences, z and z' are assumed to be fresh variables which do not introduce conflicts with the surrounding expressions.

A.1.1 Identifiers

Identifiers in CSP_Mbegin 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 ‘fnargle_’) are reserved for machine-generated code such as that produced by Casper [Lowe97].

CSP_Menforces no restrictions on the use of upper/lower case letters in identifiers (unlike some functional languages where only datatype constructors can have initial capital letters). It is, however, common for users to adopt some convention on the use of identifiers. For example

• Processes all in capitals (BUTTON, ELEVATOR_TWO)
• Types and type constructors with initial capitals (User, Dial, DropLine)
• Functions and channels all in lower-case (sum, reverse, in, out, open_door)

Note that while it is reasonable to use single character identifiers (‘P’, ‘c’, ‘T’) for small illustrative examples, real scripts should use longer and more descriptive names.

A.1.2 Numbers

Syntax

12	integer literal
m+n, m-n	sum and difference
-m	unary minus
m*n	product
m/n, m%n	quotient and remainder

Remarks

Integer arithmetic is defined to support values between -2147483647 and 2147483647 inclusive, that is those numbers representable by an underlying 32-bit representation (either signed or twos-complement). The effect of overflow is not defined: it may produce an error, or it may silently wrap in unpredictable ways and so should not be relied upon.

The division and remainder operations are defined so that, for all n except zero,

m =	n*(m/n)+m%n
|m%n| <	|n|
m%n >=	0 (provided n>0)

This states that for positive divisors, division rounds down and the remainder operation yields a positive result.

Floating point numbers (introduced experimentally for Pravda [Lowe93]) are not currently supported by FDR. Although the syntax for them is still enabled, it is not documented here. Note: the dot syntax used in communications (see section Types) can make an expression look just like a floating-point number would in other languages (e.g., ‘3.1’ is actually the pairing of two integers — the dot is not a decimal point).

The new unary minus operator can cause some confusion with comments (see section Changes from FDR1 to FDR2).

A.1.3 Sequences

Syntax

<>, <1,2,3>	sequence literals
<m..n>	closed range (from integer m to n inclusive)
<m..>	open range (from integer m upwards)
s^t	sequence catenation
#s, length(s)	length of a sequence
null(s)	test if a sequence is empty
head(s)	give first element of a non-empty sequence
tail(s)	give all but the first element of a non-empty sequence
concat(s)	join together a sequence of sequences
elem(x,s)	test if an element occurs in a sequence
<x1,... xn | x<-s, b>	comprehension

Equivalences

null(s) ≡	s==<>
<m..n> ≡	if m<=n then <m>^<m+1..n> else <>
elem(x,s) ≡	not null(< z | z <-s, z==x >
< x | > ≡	< x >
< x | b, ...> ≡	if b then < x | ...> else <>
< x | x'<-s, ...> ≡	concat(< < x | ...> | x'<-s >)

Remarks

All the elements of a sequence must have the same type. concat and elem behave as if defined by

concat(s)      = if null(s) then <> else head(s)^concat(tail(s))
elem(_, <>)    = false
elem(e, <x>^s) = e==x or elem(e,s)

Similarly, we can define palindrome to test if a sequence is its own reverse (that is ‘s == reverse(s)’) by

palindrome(<x>^s^<y>) = x==y and palindrome(s)
palindrome(_)         = true

A.1.4 Sets

Syntax

{}, {1,2,3}	set literals
{m..n}	closed range (from integer m to n inclusive)
{m..}	open range (from integer m upwards)
union(a1,a2)	set union
inter(a1,a2)	set intersection
diff(a1,a2)	set difference
Union(A)	distributed union
Inter(A)	distributed intersection (A must be non-empty)
member(x,a)	membership test
card(a)	cardinality (count elements)
empty(a)	check for empty set
set(s)	convert a sequence to a set
seq(s)	convert a set to a sequence (in arbitrary order).
Set(a)	all subset of a (powerset construction)
Seq(a)	set of sequences over a (infinite unless a is empty)
{x1,... xn | x<-a, b}	comprehension

Equivalences

union(a1,a2) ≡	{ z,z' | z<-a1, z'<-a2 }
inter(a1,a2) ≡	{ z | z<-a1, member(z,a2) }
diff(a1,a2) ≡	{ z | z<-a1, not member(z,a2) }
Union(A) ≡	{ z | z'<-A, z<-z' }
member(x,a) ≡	not empty({ z | z<-a, z==x }
Seq(a) ≡	union({ <> }, { <z>^z' | z<-a z'<-Seq(a) })
{ x | } ≡	{ x }
{ x | b, ...} ≡	if b then { x | ...} else {}
{ x | x'<-a, ...} ≡	Union({ { x | ...} | x'<-a })

Remarks

In order to remove duplicates, sets need to compare their elements for equality, so only those types where equality is defined may be placed in sets. In particular, sets of processes are not permitted. See the section on pattern-matching for an example of how to convert a set into a sequence by sorting.

Sets with a leading unary minus (most commonly, sets of negative numbers, ‘{ -2}’) require a space between the opening bracket and minus sign to prevent it being confused with a block comment (see section Mechanics).

A.1.5 Booleans

Syntax

true, false	boolean literals
b1 and b2	boolean and (shortcut)
b1 or b2	boolean or (shortcut)
not b	boolean not
x1==x2 , x1!=x2	equality operations
x1<x2 , x1>x2 , x1<=x2 , x1>=x2	ordering operations
if b then x1 else x2	conditional expression

Equivalences

b1 and b2 ≡	if b1 then b2 else false
b1 or b2 ≡	if b1 then true else b2
not b ≡	if b then false else true

Remarks

Equality operations are defined on all types except those containing processes and functions (lambda terms).

Ordering operations are defined on sets, sequences and tuples as follows

x1 >= x2 ≡	x2 <= x1
x1 < x2 ≡	x1 <= x2 and x1 != x2
a1 <= a2 ≡	a1 is a subset of a2
s1 <= s2 ≡	s1 is a prefix of s2
(x1, y1) <= (x2, y2) ≡	x1 < x2 or (x1 == x2 and y1 <= y2)

Ordering operations are not defined on booleans or user-defined types.

In the conditional expression,

if b then x1 else x2

the values x1 and x2 must have the same type. This is partially enforced by the parser. For example,

if b then {1} else <2>

is a parse error.

A.1.6 Tuples

Syntax

(1,2), (4,<>,{7})

pair and triple

Remarks

Function application also uses parentheses, so functions which take a tuple as their argument need two sets of parentheses. For example the function which adds together the elements of a pair can be written either as

plus((x,y)) = x+y

or as

plus(p) = let (x,y) = p within x + y

The same notation is used in type definitions to denote the corresponding product type. For example, if we have

nametype T = ({0..2},{1,3})

then T is

{ (0,1), (0,3), (1,1), (1,3), (2,1), (2,3) }

A.1.7 Local definitions

Definitions can be made local to an expression by enclosing them in a ‘let within’ clause.

primes =
  let
    factors(n)  = < m | m <- <2..n-1>, n%m == 0 >
    is_prime(n) = null(factors(n))
  within < n | n <- <2..>, is_prime(n) >

Local definitions are mutually recursive, just like top-level definitions. Not all definitions can be scoped in this way: channel and datatype definitions are only permitted at the top-level. Transparent definitions can be localised, and this can be used to import FDR2’s compression operations on a selective basis. For example,

my_compress(p) =
  let
    transparent normal, diamond
  within normal(diamond(p))

A.1.8 Lambda terms

Syntax

\ x1, … xn @ x

lambda term (nameless function)

Equivalences

The definition

f(x,y,z) = x+y+z

is equivalent to the definition

f = \ x, y, z @ x+y+z

Remarks

There is no direct way of defining an anonymous function with multiple branches. The same effect can be achieved by using a local definition and the above equivalence. Functions can both take functions as arguments and return them as results.

map(f)(s) = < f(x) | x <- s >
twice(n)  = n*2
assert map(\ n @ n+1)(<3,7,2>) == <4,8,3>
assert map(map(twice))(< <9,2>, <1> >) == < <18,4>, <2> >

This document was generated by Phil Armstrong on May 17, 2012 using texi2html 1.82.