The Manifest

A well-formed manifest consists of the structural elements following:

  1. The first line contains a list of labels separated by white space. These labels are used to construct variable names and structure comments that can be used in templates.
  2. Each subsequent line contains a list of values separated by white space.
  3. A value can be any literal. The absence of a value is denoted by a dash (character "-")
  4. A # character when used as the first character of a row, the row is skipped.

To illustrate the rules of forming manifests let's look at an example:

AA   BB   CC   DD   EE   XX
1    1    3    4    5
-    2   [34]  -   [56] a > 5
1    2    3    4    5    -
1    2    3    4    5    6

This manifest has five labels that allows the formation of the following substitution literals that can be used in templates:

Structured Comments

the following structured comments that match the following literals or regular expressions will be removed exposing the line for execution:

  • For the first row: "--AA1--" "--BB1--" "--CC3--" "--DD4--" "--EE5--" formed by concatenation of label and value, as well as "--AA--" "--BB--" "--CC--" "--DD--" "--EE--" derived from the fact that all variables have non-nil values (non-empty strings)
  • For the second row: "--BB2--" "--CC[34]--" "--EE[56]--" and only "--BB--" "--CC--" "--EE--" and "--XX--" since variables __AA__ and __DD__ are nil
  • For the third row: same as the first
  • For the fourth row: same as the first plus "--XX6--" and "--XX--"

Variables

The following variables and substitutions are derived:

  •  
  • __AA__ substituted by values 1 and nil (empty string) for the two rows respectively
  • __BB__ substituted by values 1 for the first row and 2 for the second row
  • __CC__ substituted by value 3 for the first row and [34] for the second row. This form is not useful for a variable, but it is very useful for a structured comment as we will see shortly
  • __DD__ substituted by value 4 for the first row and nil (empty string) for the second row
  • __EE__ substituted by value 5 for the first row and the not very useful [34] for the second row as explained earlier
  • __XX__ for the first row there is no value that corresponds to this variable, so the variable is suppressed altogether. In contrast, the third row assigns nil or empty string to the variable. For the second row the variable is substituted by the rest of the row as a single value: "a > 5".
VDM Access: 
VDM Public