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 also provides a comprehensive overview of the properties that are formally verified by Popili, but does not cover details about the verification, code generation or other tools provided by Popili that operate on Coco programs, beyond that needed to give context to the various language features. See Popili Tooling for information about Popili. This reference also does not give detailed examples to illustrate how to design software in Coco, although there are brief examples illustrating most language features. See our Introductory Tutorial as a first step for getting started with Coco.
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 |
|---|---|
| Single-threaded implementation component | |
| Single-threaded encapsulating component comprising single-threaded components | |
| Single-threaded external component | |
| Multi-threaded implementation component | |
| Multi-threaded encapsulating component comprising multi-threaded components | |
| Multi-threaded external 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 |
|---|---|
| Single-threaded provided port | |
| Single-threaded required port | |
| Multi-threaded provided 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.