Basic Constructs: Local Declarations and Definitions

Local declarations are proposed in basic specifications; local definitions are proposed in formulae. In each case, the scope of the locally declared/defined items is the remainder of the phrase only.

BASIC-ITEM        ::=   ... | LOCAL-BASIC-ITEMS
LOCAL-BASIC-ITEMS ::=   local-basic-items BASIC-ITEM+ BASIC-ITEM*

The extension introduced by a series of local basic items is required to be persistent (otherwise the specification is deemed inconsistent). The scope of the basic items declared in the first list BASIC-ITEM+ is restricted to the second list of basic items, whereas the scope of those declared in the second list BASIC-ITEM* includes the following basic items of the enclosing BASIC-SPEC.

FORMULA       ::=   ... | LOCAL-VARS 
LOCAL-VARS    ::=   local-vars VAR-DEFN+ FORMULA 
VAR-DEFN      ::=   var-defn VAR SORT TERM

A variable definition VAR-DEFN has the same effect as declaring the variable VAR to have the specified SORT, and asserting that its value is equal to that of the TERM. The scope of the variables defined in VAR-DEFN+ is the following FORMULA only.

---

CoFI Tentative Document: LanguageSummary --Version 0.95-- March 6, 1997.
Comments to cofi-language@brics.dk