2.6 Scope Rules

A scope unit is an area of specification text within which declarations may have effect, within which multiple definitions of the same name are prohibited, and outside of which declarations inside the unit do not have effect. The scope units in Larch/C++ are as in C++ (Section 3.2 of [Ellis-Stroustrup90] and Section r.3.3.1 of [Stroustrup94]), with the addition of a scoping unit for function specifications, spec-cases, and quantifiers.

The new scope units in Larch/C++ are as follows.

• [function specification] Larch/C++ function specifications (see section 6 Function Specifications) define a scope unit that is the same as a C++ local scope unit.
• [specification case] A spec-case (see section 6 Function Specifications) is a scope unit.
• [quantifier] An equality-term (see section 6.1.3 Equality Terms and Quantifiers) of the form (see section 3 Syntax Notation for details on the notation):

  quantifier [ quantifier ] ... ( term )
  

  is a scope unit.

The scope rules of Larch/C++ are exactly as in C++ (Section 10.4 of [Ellis-Stroustrup90] with the addition of namespaces as in [Stroustrup94]), with the following additions.

• [function specification scope] In a function specification (see section 6 Function Specifications), the declarations of the formals of the function, and all global variables (see section 6.7 Global Variables) in the function's specification have the usual lexical scope, analogous to C++ local scope. For example, scope of the declaration of the variable counter is the body of the specification of inc_counter.

  // @(#)$Id: inc_counter.lh,v 1.8 1997/06/03 20:30:07 leavens Exp $
  extern int inc_counter(void) throw();
  //@ behavior {
  //@   extern int counter;
  //@   requires assigned(counter, pre) /\ counter^ < INT_MAX;
  //@   modifies counter;
  //@   ensures counter' = counter + 1;
  //@ }
  

  (Unlike previous versions of Larch/C++, no exception to the usual C++ scope rules is made for function specifications. That is, global variables are visible within function specifications, and do not necessarily need to be declared as above. However, it is considered good style in a function specification to declare global variables that may be read or written.)
• [specification case scope] In a function specification, each spec-case may have a let-clause (see section 6.8 Let Clauses) which declares abbreviations for terms used in the rest of that spec-case. These declarations have the usual lexical scope, analogous to C++ local scope.
• [quantifier scope] In an assertion, quantified logical variable declarations have the usual lexical scope, analogous to C++ local scope. For example, in the following assertion the scope of i:int is the rest of the line following i:int.

  \A i: int (i < INT_MAX \implies (i < i + 1))
  

Go to the first, previous, next, last section, table of contents.