This section describes the scope rules; i.e. the rules which determine whether it is legal to redefine a particular identifier and how the compiler binds each use of an identifier to a declaration. The principles employed are:
Within this chapter, the term "function" should be taken to encompass operators and selectors also.
Identifiers in Perfect fall into the following categories:
The Perfect language is designed such that it can always be determined from context which category an identifier belongs to. Each category therefore has its own name space (meaning that at any point in the program, the same name may stand for one entity of each category).
Where an identifier is declared as the name of more than one class or type, each declaration must have a distinct signature. The signature of a class or type declaration is defined as the number of template parameters in the declaration together with the sequence of separators used to separate them.
Within a class or type template declaration, the declaration of an identifier as a parameter is considered to declare that identifier as a type name with no template parameters. Within a polymorphic function or schema declaration, an identifier which follows the keyword class in the parameter list is considered to declare that identifier as a type name with no template parameters.
It is not permitted to hide a class or class template declaration by means of a conflicting class or class template declaration in an inner block.
[Note: we could permit such hiding, but then we would have to define the rules under which it is permitted, which gets quite complicated when we consider inheritance. Or, to avoid having to make class template parameter names distinct from all visible class names and template parameter names, we could use a different syntax when referring to them, e.g. by prefixing template parameter names with class always, thereby giving template parameter names a different namespace.]
At any point in the program, an identifier may represent any number of constants, variables, let-names, functions, selectors, schemas and formal parameters, subject to the following rules provided that all of the corresponding declarations have distinct signatures.
The signature of a declaration of a variable, function schema etc. comprises two elements:
In the case of a variable, constant, parameter or let-declaration, both sequences are empty.
In the case of a polymorphic declaration, the sequence of classes will include polymorphic parameters and class or type template instantiations that depend on one or more polymorphic parameters.
A declaration with a parameter list having a repeated section is considered as having an infinite family of signatures. The members of this family are obtained by removing the keyword repeated and the following group of parameters and separators, substituting instead one or more repetitions of that group, with a comma inserted between repetitions.
Two signatures are distinct if any of the following is true:
At any point in the program, a symbol may represent any number of operators and, in the case of indexing, selectors; provided that all of the corresponding declarations have distinct signatures.
The signature of an operator declaration (or an indexing selector declaration) is a sequence of classes. For declarations that are not members, this sequence comprises the parameter types. For member declarations with no parameters, this sequence has a single entry which is the type of self. For member declarations with one parameter, this sequence comprises the type of self followed by the type of the parameter if the formal parameter follows the operator symbol in the declaration, or vice versa if the formal parameter declaration precedes the operator symbol in the declaration.
Parameter declarations involving type names, constraints or polymorphic class names are handled in the same way as for signatures of functions.
Binding in Perfect is defined in terms of dictionaries of available identifier definitions.
In each region in which identifiers may be used, there is a dictionary called the general dictionary. Every class also has two dictionaries, called the member dictionary and the non-member dictionary.
Whenever an identifier or operator symbol is mentioned other than for the purposes of declaring it, the appropriate dictionary is used to determine its meaning. If the identifier is preceded by an expression and then "." or "!" then the member dictionary for the class corresponding to the type of the expression is used; if the identifier is followed by "@" and then a class name then the non-member dictionary of this class is used; otherwise, the general dictionary is used.
Binding of an identifier name is successful if the identifier is matched with an entry in the dictionary and access restrictions do not prohibit the binding.
In describing the available dictionary, we sometimes define a new dictionary by uniting an old dictionary with a set of new declarations. The resulting dictionary contains all definitions in the old dictionary together with definitions corresponding to the new declarations.
The core of a dictionary is defined as all its class or type declarations, global constant declarations, heap declarations, and local or nonmember function, operator, selector, schema, property and axiom declarations (i.e. the original dictionary less its variable, parameter, non-global constant, and member declarations other than heaps).
The dictionary for the global declaration list is the imported environment dictionary united with the declarations in the list.
The basic general dictionary comprises the core of the dictionary for the region in which the declaration occurs, united with:
The dictionary for parameter lists, preconditions and result values is the basic dictionary.
The dictionary for postconditions and assertions is the basic dictionary united with a declaration for result .
The basic general dictionary comprises the core of the dictionary for the region in which the declaration occurs, united with:
The dictionary for parameter lists, preconditions, postconditions and assertions is the basic dictionary.
The basic general dictionary comprises the core of the dictionary for the region in which the declaration occurs, united with the declarations of the parameters.
The dictionary for the parameter list, precondition and result expression is the basic dictionary.
The dictionary for the post-assertion is the basic dictionary united with a declaration for result.
The basic general dictionary comprises the core of the dictionary for the region in which the declaration occurs, united with the declarations of the parameters.
The dictionary for the parameter list, preconditions and inherits-part is the basic dictionary.
The dictionary for the postcondition and post-assertion is the basic dictionary united with a declaration for self and the declarations of all members of the class (including all inherited members) except constructors.
The dictionary for an implementation is the dictionary for the expression or postcondition it is implementing united with the declarations in the implementation (excluding declarations within loops, conditional statements and further implementations).
Within a loop statement, the dictionary for the variable declarations following the with keyword is the dictionary for the implementation in which it occurs; the dictionary for all other regions of the statement is that dictionary united with those variable declarations.
Within a conditional statement, the dictionary for the guards is the dictionary for the implementation in which it occurs. The dictionary for each statement lost that follows a guard is that dictionary united with the declarations in the statement list (excluding declarations within loops, further conditional statements and implementations).
The dictionary within a class inherits-part comprises the core of the dictionary for the region in which the class declaration occurs united with the parameter names (if it is a template).
The dictionary for the optional class invariant directly following the inherits-part comprises that dictionary united with the non-internal members of the inherited class (including inherited members) and a declaration for self.
The dictionary for member declaration regions of a class declaration is the dictionary for the inherits-part, united with all the declarations in the region (including nonmember declarations) and all non-internal inherited members.
The dictionary for class invariants (other than those directly following an inherits-part) comprises that dictionary united with a declaration for self.
The dictionary within a bracketed expression is the dictionary for the region in which the expression occurs united with its let-declarations.
The dictionary for a predicate following ":-" and for the expression following yield is the dictionary for the region in which the construct occurs united with the bound variable declarations. Where a quantified expression declares more than one bound variable declaration, the dictionary for each bound variable declaration is the dictionary for the region united with the preceding bound variable declarations.
A class member dictionary comprises all declarations (other than nonmember declarations) of functions, operators, selectors and schemas in its abstract, internal, confined and interface sections, united with the dictionary of its parent class (if any) less the parent class internal members. Declarations in the class override declarations with identical signatures in the parent.
Each class also has a dictionary of constructors, comprising all constructor declarations in the class declaration.
Even if the use of an identifier matches an entry in the dictionary for the region in which it occurs, there may be an access restriction prohibiting binding.
There are no access restrictions to class, heap or label declarations, nor to global, local or interface declarations.
Within class member declarations, full access is permitted to members of self and it in a subjunctive expression whose initial value is self, which are declared in the same class as the current declaration, or which are defined in the confined and interface sections of ancestor classes, with the following restrictions:
Within class member declarations, access to members of objects of the same class other than self or it as above is subject to the following additional restrictions:
Access to class members from outside the class declaration is subject to the following restriction:
Where a member is declared in one section and redeclared or reimplemented in one or more other sections, it is considered as belonging to all of these sections and access to it is permitted, provided that it belongs to at least one section to which access is not prohibited.
A reference to an entity declared in an imported file is treated as a forward reference, since the order in which the compiler processes a collection of files is not defined. In practice this has little effect because the only declarations in imported files that can be referenced are global declarations.
Forward referencing of class and type declarations (other than class template parameter names) is permitted, however infinite recursion is prohibited. In particular:
Forward referencing of global and member constant and variable declarations is permitted; forward referencing of local constant and variable declarations is prohibited.
Forward referencing of function, selector, operator and schema declarations is always permitted; so long as for all circular chains of references thereby arising, an appropriate variant is declared for each declaration in the chain. However, a class invariant may not forward reference any other declaration in the same class.
Forward referencing of let-declarations and parameters is prohibited.
Forward referencing of heap and label declarations is permitted.
Perfect Language Reference Manual, Version 7.0, February 2017.
© 2017 Escher Technologies Limited. All rights reserved.