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. Functions, definitions, filters, and preserved blocks of the imported spec can be overridden by the importing spec. If a spec defines a function and uses it (e.g. in a rule or function), and another spec imports it and overrides it, uses in the imported spec use the new version. Overrides only apply locally in the spec they are declared in. Consider a spec file A containing imports from a spec file B and overrides modifying them in A. If A is again imported in a third spec file C, C will inherit the original declarations from A and B, however it will not also apply the overrides for A. If they should apply also in C, they must be repeated.

Examples

• Example for import

• use rule

• use rule with filters

• overriding imported filters

• use invariant

  • overriding imported preserved

  • adding a preserved block

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 [ "filtered" "{" id "->" expression "}" ] [ "{" { preserved_block } "}" ]

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