About This Reference

The purpose of this reference is to give a comprehensive guide to the syntax and meaning of a Coco program. That is, it describes what constitutes a valid program and what that program does. It does not give detailed examples of how to write useful Coco programs, although there are brief examples illustrating most language features; nor does it give a formal account of the language semantics. It also does not give information about the verification and code generation tools that operate on Coco programs, beyond that needed to give context to the various language features.

Grammatical Conventions

This reference includes grammar-like fragments describing the form of Coco syntax. Chevrons (« and ») are used to delimit “nonterminals”, which ought to be replaced with the entity described, rather than entered literally. Plural nonterminal names indicate that zero or more singular nonterminals may be entered, which are separated by a comma unless specified otherwise. For example, «parameters» indicates that zero or more parameters may be entered.

As is usual in BNF, square brackets ([]) indicate that their contents are optional, while a vertical bar (|) indicates that either what is on its left or what is on its right may be entered.

Graphical Conventions

This reference uses the following graphical conventions for components to denote their type and runtime:

Component Meaning
Component Single-threaded implementation component
Component Single-threaded encapsulating component comprising single-threaded components
Component Single-threaded external component
Component Multi-threaded implementation component
Component Multi-threaded encapsulating component comprising multi-threaded components
Component Multi-threaded external component
Component Multi-threaded encapsulating component comprising single-threaded components

Similarly, the following graphical conventions are used for ports to denote their runtime, and whether they are provided or required ports:

Port Meaning
port Single-threaded provided port
port Single-threaded required port
port Multi-threaded provided port
port Multi-threaded required port

Errors in Coco Programs

Broadly speaking, there are two types of program errors considered in this reference:

Static errors
are those that will always be detected by a compiler or code generator. Examples include syntax errors and type errors.
Dynamic errors
are those that would occur if the program was run, or whose absence could be proved by a verification tool. Examples include out-of-bounds array accesses, assigning too large or too small a number to a bounded integer type and violating the specified behaviour of a port.