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*

Discharged: Instead of this, we have locality attributions in SIG-DECLs. This seems to be forced if we adopt non-linear visibility.

The extension introduced by a series of local basic items is required to be persistent (otherwise the specification is deemed inconsistent).

Discharged: With non-linear visibility, this requirement makes no sense.

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.

[DTS] Restrictions must be imposed to ensure that the resulting signature is well-formed. For example,

local sort s in function f:s->s

should not be allowed. The presence of subsorts might complicate this issue.

Discharged: With locality attributes, such a restriction is still required.

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.

[TM] What is the semantics of let x:s=t in phi? I can see two possibilities:

1. forall x:s . x =^e t => phi
2. exist x:s . x =^e t /\ phi

Both are equivalent if t is defined. If t is undefined, the first is true and the second is false.

Discharged: Local definitions are not included.

---

CoFI Note: S-1 --Version 1.3-- 25 April 1997.
Comments to cofi-semantics@brics.dk