Documentation

This section provides a summary of the documentation format supported by Coco for documenting Coco programs. Documentation comments written in Coco have two main uses:

  • They are displayed inline when relevant in the Coco Platform tooling. For example, Eclipse shows the documentation during code completion.
  • They are preserved in the generated code for each target language in a format that enables standard documentation generation tools to be used. For example, the C++ generator inserts the corresponding comments in a form that is compatible with Doxygen.

Coco supports documentation comments written using a subset of CommonMark. In order for Coco to distinguish between standard comments and documentation comments:

  • /// starts a single-line documentation comment, which finishes at the end of the line.
  • /** starts a multi-line document comment, which finishes at the matching */.

This section only describes what is permitted within documentation comments such as the above: standard comments (i.e. those starting with just // or /*) are not affected by this, and will be ignored by all Coco tooling.

Format

Within the comments, the standard Markdown rules are supported: Paragraphs are denoted by inserting blank lines between them; numbered lists are specified using numerals (e.g. 1, 2, 3) followed by a full-stop (1.) or a right parenthesis (1)); bullet point lists are specified by the characters -, +, or *; and headers are denoted with #, or by underlining them with = and -.

Declarations

Coco supports some special Markdown elements specifically for documenting declarations in a structured form. A declaration is documented by inserting a single- or multi-line documentation comment immediately before it. For example:

/**
 * External type representing error codes for the failure cases.
 */
external type ErrorCode

/// Values represent the success or failure (with error codes) of the system.
enum Outcome {
  case Pass
  case Fail(error : ErrorCode)
}

In this example, documentation comments are specified for the external type and enum declarations. When hovering the cursor over the ErrorCode type used in Outcome, a tooltip will appear with the documentation comment for ErrorCode. The same applies when the type Outcome is used in a declaration elsewhere in the code:

port P1 {
  /// Checks the status of the system.
  function check() : Outcome

  machine {
    check() = nondet {
      Outcome.Pass,
      Outcome.Fail(_),
    }
  }
}

In this example, port P declares a function interface called check() with return type Outcome. When hovering the cursor over Outcome, the documentation for Outcome will pop up as a tooltip. This example also illustrates how these comments can be nested, such as the comment specified for the nested declaration of check().

Coco also supports a number of special paragraphs within declaration comments, as follows:

Parameters

A parameter is documented using the following syntax within a documentation comment:

- parameter «identifier»: «description»

Multiple parameters can also be documented using the following syntax:

- parameters:
  «parameters»

«parameter» := - «identifier»: «description»

The following example illustrates the use of documenting parameters in a simple function declaration:

/// Toggles the value between 0 and 1, and returns the same value for all other integers.
///
/// - parameters:
///   - x: value to be toggled.
function safeToggle(x : Int) : Int = {
  match (x) {
    0 => 1,
    1 => 0,
    _ => x,
  }
}

In this example, parameter x in the function declaration safeToggle is documented. When hovering over instances of x in the function body this documentation will appear as tooltips. Similarly, when the function safeToggle is called in other parts of the code, the documentation for the function and its parameters will also appear as tooltips.

Return Values

Return values of a function are documented in a similar way to parameters with the following syntax:

- returns: «description»

The following example illustrates how the return value of a function is documented:

port P2 {
  /// Checks the system is idle.
  ///
  /// - returns: true if the system is idle, and false otherwise.
  function isIdle() : Bool
  function begin() : Nil

  machine {
    state Idle {
      begin() = setNextState(Running)
      isIdle() = true
    }
    state Running {
      isIdle() = false
    }
  }
}

In this example, the return value of the function isIdle() is documented. These comments will appear in the documentation tooltips for the function isIdle when called in other parts of the code.

Other fields

In addition to parameters and return, Coco supports other simple fields which can be used to provide structured documentation. The syntax for these fields is as follows:

- «doc field»: «description»

where description is an arbitrary textual description, and where doc field is one of the following:

  • author
  • bug
  • copyright
  • invariant
  • note
  • postcondition
  • precondition
  • remark
  • returns
  • seealso
  • since
  • todo
  • warning

The following example illustrates how the return value of a function is documented:

/// Checks the value.
///
/// - precondition: x must be a natural number
function check(x : Int) : Nil = {}