Note

You are not reading the most recent version of this documentation. 1.4.7 is the latest version available.

Lexical Conventions¶

Coco File Encoding¶

Coco files must be UTF-8 encoded.

Comments¶

Coco supports comments in the style of C++:

// starts a single-line comment, which finishes at the end of a line.
/* starts a multi-line comment, which finishes at */. Multi-line comments may be nested.

Coco is otherwise not whitespace-sensitive: multiple consecutive whitespace characters behave identically to a single one.

Keywords¶

The keywords of the language are:

abstract	after	as	assertion
async	attribute	attributes	await
become	behaviour	break	case
class	component	continue	defer
else	entry	enum	execution
exit	external	final	for
function	if	illegal	import
in	incoming	inherit	init
inout	instance	interleave	internal
machine	match	module	monitor
mut	mutable	mutating	nondet
object	offer	optional	otherwise
out	outgoing	periodic	port
private	property	protected	public
return	signal	spontaneous	state
static	struct	test	testcase
trace	trait	type	unqualified
val	var	verify	where
while

Identifiers¶

Identifiers are used to give names to entities. In Coco, an identifier must begin with a capital or lowercase letter (i.e. A to Z or a to z), or an underscore (_), and can be followed by letters, digits (0 to 9), or underscores (_) only.

syntaxIdentifier¶

«identifier» := «alpha»[«alphanum»]
«alpha» := A..Z | a..z | _
«alphanum» := «alpha» | 0..9

syntaxDot Identifier List¶

«dot identifier list» := «identifier»[.«dot identifier list»]

A compound identifier is a non-empty sequence of identifiers separated by a dot (.). Compound identifiers are used to qualify identifiers within a particular namespace.

Literals¶

There are three kinds of literals in Coco, namely integer, character and string literals.

syntaxLiteral¶

«integer» | «character» | «string»

where:

integer represents integer literals, consisting of the digits 0-9.
character represents character literals, consisting of a single UTF-8 encoded character enclosed by single quotes (').
string represents string literals, consisting of UTF-8 encoded characters enclosed by double quotes (").

The following escape sequences are also supported for character and string literals: newline (\n), carriage return (\r), horizontal tab (\t), null (\0), backslash (\\), double quotation mark (\"), and single quotation mark (\').