Import and Use Statements

Contents of additional spec files can be imported using the import command. Some parts of the imported spec files are implicitly included in the importing spec file, while others such as rules and invariants must be explicitly used.

Todo

This feature is currently undocumented.

Syntax

The syntax for import and use statements is given by the following EBNF grammar:

import ::= "import" string

use ::= "use" "rule" id
        [ "filtered" "{" id "->" expression { "," id "->" expression } "}" ]
      | "use" "builtin" "rule" id
      | "use" "invariant" id [ "{" { preserved_block } "}" ]

See Basic Syntax for the string and id productions, Expressions for the expression production, and Invariants for the preserved_block production.