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
use
d.
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.