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 enum entry execution exit external final for function if illegal in incoming inherit init inout instance interleave internal import machine match module monitor mut mutable mutating nondet object offer optional otherwise out outgoing periodic protected private public return port property signal spontaneous state static struct test testcase trait trace 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 (\').