ABSTRACT
Every identifier in a VDM-SL specification is introduced at a specific occurrence, which may be called its declaration. The declaration also associates the identifier with an entity: a value, function, variable, and so on. This association holds over a region of VDM-SL text called the scope of the declaration, within which (with exceptions noted below) any use of the identifier denotes the associated entity. In certain cases an identifier may be reused within the scope of one declaration to denote a different entity, by a declaration with a nested scope. Within the inner scope, the outer declaration is hidden. VDM-SL also allows identifiers in certain cases to be used to denote more than one entity within the same scope; in these cases the different uses are syntactically distinguishable.
