Many programming languages allow programmers to regulate accessibility;
i.e., annotating a declaration with keywords such as  and  to indicate where it can be accessed.
Despite the importance of name accessibility for, e.g., compilers, editor auto-completion and tooling, and automated refactorings,
few existing type systems provide a formal account of name accessibility.

We present a declarative, executable, and language-parametric model for name accessibility, which provides a formal specification of name accessibility in Java, , , Rust, and Eiffel.
We achieve this by defining name accessibility as a predicate on resolution paths through scope graphs.
Since scope graphs are a language-independent model of name resolution, our model provides a uniform approach to defining different accessibility policies for different languages.

Our model is implemented in Statix, a logic language for executable type system specification using scope graphs.
We evaluate its correctness on a test suite that compares it with the , Java, and Rust compilers,
and show we can synthesize access modifiers in programs with holes accurately.

§ INTRODUCTION

Many programming languages, especially object-oriented ones, support information hiding, , regulating from which positions in a program a declaration can be accessed.
Information hiding is used to enforce invariants of particular code units, implement design patterns (e.g. the singleton pattern), improve modularization, limit public APIs to offer guidance to library users and guarantee forward compatibility.

Support for information hiding is usually provided using access modifier keywords
[Other common names include `access specifier' or `visibility modifier'.]
(access modifiers for short), such as , ,  and .
Each of these corresponds with a particular accessibility policy that is validated by the type checker.

Although recent research has not paid much attention to access modifiers,
there are still good reasons to study their semantics.
First, understanding access modifiers is required to implement (alternative) compilers and editor services correctly.
In particular, disregarding accessibility may result in incorrect name binding, and hence incorrect program behavior.
Second, formalizing access modifiers enables reasoning about the meaning of programs.
Finally, program transformation tools, such as automated refactorings, must handle the semantics of accessibility correctly.
This is especially relevant for research on large-scale automated transformations, aimed at dealing with large (legacy) codebases.
It is often infeasible to check transformations performed with such tools manually.
Thus, the correctness of these transformations must be guaranteed through other means.

Inheritance through Packages.

Inaccessible or Shadowed?

Accessibility and Shadowing.

Examples of intricate Access Modifier semantics. Classes are assumed to be public.

The meaning of access modifiers can be intricate in corner cases.
We illustrate that using the examples in <ref>.
In <ref>, there is an inheritance chain, where class C extends class B, which itself extends A.
Classes A and C reside in package p1, while B is in p2.
Class A defines a package-accessible field x, which is accessed in C.
The question here is whether that access is actually allowed.
One could reason that it is correct, as the access occurs in the same package as the declaration, so a package-level declaration should be visible.
On the other hand, one could consider x not inherited by B <cit.>, and thus not inherited by C either.
In fact, the Java language designers chose the second option, rejecting this program <cit.>.
Using  is accepted however.

Something similar happens in <ref>.
Here, one can consider the reference x in class C to be invalid, as the field in class B is inaccessible.

Alternatively, under the assumption that B.x is out of scope, the reference can be valid, pointing to A.x.
In this case, Java checks accessibility after shadowing, so this program is again rejected.
However, in <ref>, accessibility does influence the binding.
The reference x binds to the field of the enclosing class B, as the field inherited from class A is inaccessible.
However, reference y binds to the field inherited from A.
Thus, in this case, the accessibility of the inherited fields determines the resolution of x and y; , accessibility is checked before shadowing.
This shows that specifying accessibility is essential to defining the name binding of a language correctly.

Unintuitive semantics of accessibility occurs in non-object-oriented languages as well.
For example, the accessibility scheme of Agda seems simple: definitions are either public or module-private, and imported definitions can be re-exported.
However, issue #5461[<https://github.com/agda/agda/issues/5461>] reports that re-exports in a private block are still exposed to the outside world.
While this intuitively seems wrong to most commenters, an argument is made that this is actually the intended behavior.
The discussion stalls shortly after a remark that talking about intended behavior is “meaningless without a specification”.

These examples show that the meaning of access modifiers is not always obvious.
Hence, language designers should define their semantics unambiguously.
Ideally, that is done through specifications containing inference rules.
Inference rules allow unambiguous interpretation of the meaning of programming language constructs, including name binding.
However, perhaps surprisingly, a general model for defining access modifiers has never been proposed.

Perhaps closest is the work of Steimann and Thies <cit.> (later incorporated in the JRRT refactoring tool <cit.>).
They propose a constraint-based approach to automating refactorings in Java, by collecting and solving accessibility constraints.
These constraints are generated using constraint generation rules, which cover the access rules the Java compiler enforces.
By solving these constraints, changes in accessibility implied by the refactoring can be inferred, yielding type- and behavior-preserving refactorings.

Steimann and Thies' work solves the problem of making refactorings in Java sound regarding accessibility.
However, it does not yet give a high-level explanation of the meaning of access modifiers.
This is partly because the constraint generation rules need several low-level details to catch some intricate corner cases,
but also because the function that computes the minimal required accessibility level is not given, as it was “unpleasant to specify” and “of no theoretical interest” <cit.>.
Therefore, their work cannot easily be adapted to a different language or a different application (, a type checker).

To advance the state of the art, we pursue the following goals:

* Explain the meaning of access modifiers.

* Explain the (subtle) differences between access modifiers in different languages.

* Provide a framework for experimenting with feature combinations that do not (yet) exist in other languages.

To this end, we do not fully formalize one particular language, but rather define a toy language that incorporates and combines a large number of accessibility features.

To abstract over low-level name resolution details, we use scope graphs <cit.>.
In this paper, we demonstrate this is a natural fit, because accessibility can be expressed as a predicate over paths in a scope graph.

The specification is written in the logic language Statix <cit.>, which has a well-defined declarative semantics and also supports generating executable type-checkers automatically.

We compare these executable type checkers with reference compilers of Java, , and Rust, showing that we accurately captured the semantics of access modifiers in some real-world languages.
Moreover, using Statix/scope graphs as a basis for (language-parametric) refactorings is an active topic of research <cit.>.
We envision that this will provide accessibility-aware refactorings similar to Steimann et al., without requiring significant additional effort.
This is substantiated by the fact that Statix-based code completion <cit.> proposes an access modifier if and only if it would not cause accessibility errors elsewhere in the program.

In summary, the contributions of this paper are as follows:

* We provide a systematic classification of accessibility features (<ref>);

* we apply our taxonomy to Java, , , Rust, and Eiffel (<ref>);

* we present a specification of (various versions of) accessibility on
modules (<ref>),
subclasses (<ref>), and
their conjunctive and disjunctive combination (<ref>);

* we extend our specification with accessibility-restricting inheritance (<ref>);

* we prove some theorems about our model, showing it is well-behaved (<ref>); and

* we implement our specification in Statix, and compare it with the standard compilers of Java, , and Rust.
Moreover, we show access modifiers can be synthesized accurately using Statix-based Code Completion <cit.> (<ref>).

extendedThis paper comes with an artifact that allows reproducing the evaluation <cit.>, and appendices containing a full specification of the access modifiers and proofs of the stated theorems <cit.>.

§ ACCESS MODIFIERS IN REAL-WORLD LANGUAGES

In this section, we explore the design space of access modifiers as they occur in real-world languages.
We first motivate why languages have access modifiers (<ref>).
After that, we discuss common accessibility features (<ref>), summarizing them in a feature model (<ref>).

§.§ Why Accessibility?

Most programming languages allow programmers to define entities (variables, functions, types, etc.), and assign a name to them.
That name can then be used to refer to the introduced entity from other positions in the program.
However, as there is typically a large number of entities within a software project, most languages offer a notion of modularization to group related definitions.
Equally named definitions in different modules can be distinguished by qualifying them with the name of the module in which they reside.
Unqualified (or partially qualified) names by default resolve within their enclosing module, or imported modules.
Details of this scheme differ from language to language, but generally aim to make definitions easy to refer to (, by minimizing the number of required qualifiers), while trying to be unambiguous to the compiler and the programmer.

However, these rules may often be too lenient with respect to the intention of the programmer.
A definition may be accessible from scopes where it is not intended to be used.
This can have detrimental effects on the quality of a software artifact.

For example, exposing all internal definitions of a library makes it
(1) less intuitive to its users,
(2) prone to forward compatibility issues and technical dept (strong coupling).

For these reasons, many programming languages provide constructs that give the programmer control over the regions of code where a definition can be accessed.
For example, in many object-oriented languages, a class can access fields from its ancestor classes by default (language-controlled).
However, if the programmer does not want a field to be accessible from subclasses, they can add a  access modifier.
This modifier prevents access from all other classes (programmer-controlled).
Although many constructs that provide access control to the programmer can be envisioned, most languages settle on a limited set of keywords that can be attached to a definition.

In practice, this relatively simple scheme has proven powerful enough to cover most use cases.

§.§ Accessibility in Practice

Next, we explore how languages typically provide modularization and accessibility features.

A common feature that provides modularization is modules (also called `package' or `namespace').

A module is a syntactic

construct that introduces a named collection of definitions.
Members of modules can be accessed using the name of the module, for example in a preceding import statement, or as a qualifier to the name of the member that is accessed.

Hiding a definition from other modules is the simplest accessibility restriction that can be applied with respect to modules.
For example, Java declarations without an access modifier can only be accessed within the same package.
Rust items without a modifier behave similarly, except that declarations can still be accessed from submodules.

Some languages have multiple notions of modularization.
For example, has assemblies, namespaces, and files, where a namespace can comprise multiple files, and/or a file can contain multiple namespaces.
The  keyword in restricts accessibility to the assembly, and the  keyword (introduced in 11 <cit.>) to the current file.
Similarly, Java 9 introduces modules <cit.>, with features to restrict access from external modules.

Some languages give some more control over which modules a declaration can be accessed from.
For example, Rust has the  path access modifier, where path refers to some enclosing module.
This enables programmers to expose items to an arbitrary ancestor.

Imports usually do not affect the visibility of a declaration.
A notable exception to this rule is re-exporting (e.g., as implemented in Rust), which can actually change the visibility of a declaration, as shown in <ref>.
In this program, the module  is accessible in , but not in its parent (the root scope).
Therefore, the function  cannot access its field .
However,  re-exports , which gives rise to a new definition .
As  is accessible in the root scope, so is this definition.
Hence, via the re-export,  can access , although the original declaration was hidden.

From an accessibility point of view, re-exporting can typically be considered as a combination of an import and a declaration, where the declaration always points to the imported member.
The re-exported item ( in the example) should be accessible from the location of the re-export.
References to the re-export should have access to the location of the re-export, but not necessarily to the location of the original declaration.
In fact, for any access path, it does not matter whether the declaration is a re-export or not.

A special modularization concept is the notion of classes,
which represent composite data types with associated operations (methods).

Where simple modules only have a static interpretation, an arbitrary number of class instances can exist at runtime.
At this point, we slightly over-simplify the reality.
For example, neither parameterized modules (ML) nor  (e.g. Scala/Kotlin) fit in this scheme.
We made this choice deliberately, to cover the most prevalent cases.
We conjecture that the techniques we develop for classes can be applied to parameterized modules
(and vice versa for modules and objects)
but leave explicating that to future work.

While modules can implicitly be related to each other by their relative position, such a relation does not exist for classes.
However, classes can extend other classes, ensuring the subclass inherits the fields of its parent class.
This creates an inheritance hierarchy orthogonal to the module hierarchy.

Object-oriented languages usually provide modifiers to control accessibility over the inheritance chain.
For example, Java and have a  keyword, which prevents access outside the defining class.
Additionally, the  keyword allows access from subclasses, but prevents access from any other location.

In Java and , the accessibility level is inherited with the field.
That means, if a field in the superclass is , it will be protected in the subclass as well.
However, allows restricting the accessibility of members of the parent class.
A  modifier on extends-clauses will make all inherited public/protected members private on instances of the subclass.
Similarly, a  modifier will make all inherited public members protected.

Finally, some languages allow specifying `friend' classes, which grant the friend access to its members.
This enables fine-grained access control, independent from module and class hierarchies.
While discouraged in , Eiffel provides only this access control mechanism.

Accessibility restrictions on modules and classes be combined.
This is very explicit in , which

has  and  as additional modifiers.
The former permits access from within the assembly (similar to ) and to subclasses (similar to ), even if they live outside the assembly.
Analogously,  grants access to subclasses in the same assembly only, which is equivalent to the conjunction of  and .

§.§ Classification

These concepts are organized
and related
in the feature model in <ref>.
Following the previous discussion, the main features are modules and classes.
We have only a single feature for modules, because the different variants are (apart from s files and namespaces) typically not mutually nested.
The  keyword can either relate to the containing module (Direct) or an arbitrary parent module (Ancestor).
We explore this further in <ref>.

In the Classes category, the three subfeatures denote the three mechanisms for access control:
Friends allow access to other classes by name,
Subclass Access Modifiers are access modifiers on definitions that determine how it is accessible within the class hierarchy (<ref>), and
Extends Clause Access Modifiers (<ref>) are access modifiers on extends clauses, as seen in .
The latter two have subfeatures for each concrete keyword associated with the access control mechanism.
For that reason,  and  occur twice: once on definitions and once on extends clauses.
<Ref> classifies several languages according to this scheme.
In the remainder of this paper, we develop AML (Access Modifier Language), a language that covers all features.
To this end, we first introduce scope graphs (<ref>), and a base language for AML (<ref>).

§ USING SCOPE GRAPHS TO MODEL NAME BINDING IN PROGRAMS

In the previous section, we sketched the landscape of access modifiers.
This discussion was based largely on prose specifications as well as experiments with compiler implementations.
No language specification we are aware of provides a more rigorous model of accessibility (or even non-lexical name binding).
In this section, we introduce scope graphs <cit.>, and argue that they provide a suitable framework for such a model.

<Ref> introduces AML (Access Modifier Language), a toy language with a type system defined using scope graphs.
<Ref> will extend this language with all accessibility features from <ref>.

§.§ Scope Graphs as A Model for Name Binding

From a name binding perspective, classes and modules have some similarities.
Each of these constructs can be thought of as introducing a `scope' (region of code), in which declarations live, and in which names can be resolved.
Scopes are related to each other in various ways.
First, modules are related according to their relative position in the abstract syntax tree.
In addition, imports and extends clauses relate arbitrary modules and classes, respectively.
Resolving a reference corresponds to finding a matching declaration in a scope that is reachable from the scope of the reference.
For example, a reference may resolve to a declaration if it lives in a lexically enclosing scope, or in a module that is imported in an enclosing scope.

Scope graphs <cit.> make this more precise.
In this model, the name binding structure of a program is represented by a graph.
<Ref> (adapted from Poulsen et al. <cit.>) gives an example program and its corresponding scope graph.
A scope is represented by a circular node in the graph.
For example, $\xrootscope$ represents the global scope, and $\xscoperef{A}$, $\xscoperef{B}$ and $\xscoperef{C}$ represent the bodies of modules 𝕀A, 𝕀B, and 𝕀C, respectively.
Scopes are related using labeled, directed edges.
For example, $\xscoperef{A}$ is lexically enclosed by $\xrootscope$, and thus the graph contains an edge from $\xscoperef{A}$ to $\xrootscope$ with label $\lblLEX$.
Similarly, $\xscoperef{B}$ imports $\xscoperef{A}$, and thus the graph contains an edge $\xscoperef{B} \scopeedget[\lblIMP] \xscoperef{A}$.
Finally, scope graphs contain declarations.
For example, a declaration of  in scope $\xscoperef{C}$ is represented by the $\xscoperef{C}\ \typeedgeg[\lblVAR]\ \texttt{i} : \tyINT$ edge/node pair.
Similarly, the modules are declared in the root scope (, $\xrootscope \typeedget[\lblMOD] \id{A} \sim \xscoperef{A}$).
The language specification determines which data is included in the declaration.
Similarly, the labels for edges and declarations can be chosen to match the (binding) constructs of the language.

To resolve a reference, a query is executed to find a valid path in the scope graph from the scope of the reference to a matching declaration.
Queries give specification writers several options to filter paths, to retain only valid paths.

First, a unary predicate selects valid declarations.
Usually, this predicate matches declarations with the name of the reference.
Second, a regular expression over labels is used to select valid paths.
This regular expression can, for example, be used to prevent transitive imports, or accessing members in a lexical parent of an imported module.

<Ref> illustrates this with the query for 𝕀i in module 𝕀C (dashed blue box).
The parameter on the arrow ($\mathsf{\lblLEX}^{*}\mathsf{\lblIMP}^{?}\mathsf{\lblVAR}$), is a regular expression that defines which paths to declarations are valid.
The $\mathsf{\lblLEX}^{*}$ indicates that a path may traverse an arbitrary number of $\lblLEX$-edges.
This corresponds to looking for variables in enclosing scopes.
Next, the $\mathsf{\lblIMP}^{?}$ part indicates that zero or one $\lblIMP$-edges can be traversed.
Finally, the regular expression ends with $\lblVAR$ to ensure all paths resolve in variable declarations only, excluding modules.
The $\mathsf{isVar}_{\id{i}}$ parameter matches all variable definitions with name 𝕀i ($\mathsf{isVar}$ is defined in the next section).
The candidate path (shown as blue edges) does not match this regular expression.
Because $\lblIMP$-labeled edges may only be traversed one time, the step to A cannot be made.
In other words: the declaration of 𝕀i in 𝕀A is not reachable from 𝕀C.

Not every declaration that is reachable (, for which a valid access path exists) can actually be referenced, due to shadowing.
For example, in most languages, local definitions have higher priority than imported ones.
We call reachable declarations that are not shadowed by any other declaration visible.

In scope graphs, visibility can be encoded using a partial order on labels.
For example, an order $\lblVAR < \lblIMP$ encodes that (local) variable declarations shadow imported declarations.
This is illustrated in <ref>.
The reference 𝕀x in module 𝕀F can refer to the declaration in module 𝕀D as well as the one in module 𝕀E.
Because the label order (third argument) indicates that imports shadow lexically enclosing scopes ($\lblIMP < \lblLEX$).
Thus, the variable resolves to the declaration in $\xscoperef{F}$.
Alternatively, if $\lblLEX < \lblIMP$, it would resolve to 𝕀x in $\xscoperef{D}$.
Finally, if neither $\lblLEX \not< \lblIMP$ nor $\lblIMP \not< \lblLEX$, both paths would be included in the query result.

In summary, scope graphs model the name binding structure of a program using nodes for scopes and declarations, and edges for relations between those.
Queries can be used to model reference resolution.
A query selects a declaration when
(1) it matches some predicate, and
(2) there exists a path to it of which the labels match a regular expression, and
(3) no other paths that traverse labels with higher priority exist.
The result of a query is a set of paths that lead to these matching declarations.

We can model extensibility using plain scope graphs by including accessibility information in the declaration.
In other words, a declaration of a variable in a scope graph contains not only a name and a type, but also its accessibility level.
After resolution, we check if the path that the query returns is actually valid according to the accessibility level of the declaration.
For example, if a variable is private, but an $\lblEXT$-edge (for class extension) is traversed, an error is emitted.
With this pattern, we can model all accessibility features.

<Ref> introduce the graphical notation of scope graphs.
In text, variable $s$ ranges over scopes, and $S$ over sets of scopes.
Moreover, we use the following notation for assertions on scope graphs:
$s_1 \scopeedget[\mathsf{L}] s_2 \in \SG$ means `scope graph $\SG$ has an $\mathsf{L}$-labeled edge from $s_1$ to $s_2$', and
$s \typeedget[\mathsf{D}] d \in \SG$ means that $\SG$ has a declaration with data $d$ under label $\mathsf{D}$ in scope $s$.
Moreover, we write queries in the following way:

where $\SG$ is the scope graph in which the query is resolved,
$s$ is the scope in which the resolution starts,
$\re$ is the regular expression that paths must adhere to,
and $\mathcal{P}$ is the predicate that declarations must match.
$\mathcal{O}$ is the strict partial order on labels used for shadowing.
It is usually written as $\mathsf{L}_1 < \mathsf{L}_2 < \cdots < \mathsf{L}_n$.
We omit the label order when there is no shadowing.
$R$ is the result set containing tuples of paths and declarations.
When we expect a single result, we use $\setOf{ \langle p, d \rangle }$ to match on the value in the set.
Paths are alternating sequences of scopes and labels, written as $s_1 \pathstept[\mathsf{L}_1] s_2 \cdots s_m$.
Paths do not include the declaration it resolved to, but stop at the scope in which the declaration occurs.
The functions $\mathsf{src}(p)$, $\mathsf{tgt}(p)$ refer to the source and target scope of a path, respectively.
$\mathsf{scopes}(p)$ denotes all scopes in a path.

§ AML: THE BASE LANGUAGE

In the next sections, we show how scope graphs support intuitive formalization of accessibility.
We will do so by defining AML (Access Modifier Language).
The base syntax (which will be extended later) is given in <ref>.
In AML, a program consists of a list of modules.
Each module can define other modules, import other modules, and contain class definitions.
A class can optionally extend another class, and contains a list of field declarations.
Each field has an access modifier, and is initialized by some expression.
Possible expressions include references, integer constants, class instance creation, field access, and binary operations.

At the right-hand side of <ref>, the scope graph parameters are shown.
There are three labels that connect scopes.
denotes lexical scoping, denotes imports, and class extension.
The other three labels are used for declarations.
is used for module declarations, for classes, and for variables/fields.
Next, we assume that each module scope has a edge pointing to itself, and similarly, each class has a scope pointing to itself.
This will be used to resolve enclosing classes or modules.
The sort d denotes the data that can be associated with scopes.
Modules and classes are characterized by their name and the scope of their body.
A field has a name, a type T, and an accessibility level A.
Scopes that are not declarations implicitly map to themselves.
To query declarations, we use the four predicates shown at the top of <ref>, which each match a single kind of declaration.
Depending on the type of access control we formalize, different access modifiers will be used.
Therefore, we have left the acc and A productions partially unspecified.
Each section will instantiate those appropriately.

Typing Rules

<Ref> presents some typing rules of AML.

The rules are written in a declarative style, where a scope graph $\SG$ that models the program is assumed.
Constraints over the scope graph are used as premises.
The highlighted premises show where accessibility is integrated into the type system.
We now discuss each of the presented rules.

The d-def rule asserts a declaration is well-typed if the initialization expression $e$ has some type $T$ (first premise),
the access modifier acc corresponds to some accessibility policy A (second premise), and
an appropriate declaration exists in the scope graph (third premise).
The accessibility policy is included in the declaration, which enables us to validate accessibility when type checking references.

Next, rule t-var defines how references are type checked in a current scope $s$.
First, it performs a query that looks into the lexical context ($\reclos{\lblLEX}$), parent classes ($\reclos{\lblEXT}$), and eventually resolves to a variable declaration ($\lblVAR$).
It matches only variables with the same name as the reference ($\mathsf{isVar}_x$).
Regarding shadowing, it prefers local variables over variables from a parent class ($\lblVAR < \lblEXT$), and
variables from parent classes over variables from enclosing classes ($\lblEXT < \lblLEX$).
The query should return a single result, as the name would otherwise be ambiguous.
From this result, the access path $p$, type $T$, and accessibility policy $A$ are extracted.
The path and the accessibility policy are used in the second (highlighted) premise ($\premMAcc{\SG}{s}{p}{A}$), which asserts that `accessibility policy $A$ grants access via path $p$ in scope $s$'.
In future sections, we will define new accessibility policy rules, that may prohibit access of a variable, even if the query premise resolved properly.

Note that, by having accessibility separated from the resolution, we do not capture the interaction between accessibility as shown in <ref>.
We made this choice because the place where accessibility is integrated does not influence the access rules themselves, and this presentation allows more concise derivations, which makes the explanations more accessible.
subsec:full-path-orderA.1 shows how to integrate accessibility in the shadowing policy of a query, and is incorporated in the evaluation (<ref>).

For this base language, we only have the  access modifier.
The a-pub rule shows that this keyword corresponds to the policy.
The meaning of this policy is that access is allowed from any location, with any access path.
This is encoded in the ap-pub rule, which has no premises.

Finally, the last two rules define how references to classes and modules are resolved.
Rule q-mod indicates that module reference $x$ resolves to scope $s_m$ if that scope is included in the closest module declaration with name $x$ in the lexical context.
Similarly, a class reference resolves to the scope of the closest class declaration $s_c$, preferring (non-transitively) imported classes over classes in the lexical context (q-cls).

The example in <ref> shows two classes 𝕀A and 𝕀B.
Both classes have a $\lblTHIS$-edge pointing to itself.
Class 𝕀B extends class 𝕀A, which is represented by the $\xscoperef{B} \scopeedget[\lblEXT] \xscoperef{A}$ edge in the scope graph.
Class 𝕀A has a public field 𝕀i with type $\tyINT$.
The type as well as the corresponding access policy are included in the scope graph declaration.
Similarly, class 𝕀B has a field 𝕀j.
The initialization expression of 𝕀j references 𝕀i, which is represented with the query shown in the dashed box.

<Ref> shows the part of the typing derivation that checks the highlighted reference.
Reference 𝕀i is type checked in scope B, and has type $\tyINT$.
The first premise repeats the query shown in the scope graph, with the parameters and result made explicit.
In particular, the resolution path is $\xscoperef{B} \pathstept[\lblEXT] \xscoperef{A}$.
The validity of this path is checked by the second premise, which is satisfied by the ap-pub rule.

Auxiliary Relations

Finally, <ref> presents some auxiliary relations that we will use later.
First, the $\premEncM{\SG}{s}{S_M}$ relation asserts that $S_M$ is the set of scopes of the enclosing modules of $s$.
It is defined as a query that looks for a $\lblTHISMOD$ edge in the lexically enclosing scopes.
There is no shadowing, so $R$ can contain multiple results in the case of multiple nested modules.
The result $R$ is translated to the set of module scopes by discarding the access paths.

This relation is inhabited for any enclosing module scope.
The second relation $\premEncMI{\SG}{s}{s_m}$ is only inhabited for the innermost enclosing module $s_m$.
The query in its definition finds the closest $\lblTHISMOD$-edge, which is enforced by the shadowing policy $\lblTHISMOD < \lblLEX$.
Thus, the query returns only one result, from which the module scope $s_m$ is extracted.

Analogously, $\premEncC{\SG}{s}{S_C}$ relates $s$ to all enclosing class scopes $S_C$, and
$\premEncCI{\SG}{s}{s_c}$ is satisfied if $s_c$ is the innermost enclosing class of $s$.

§ DEFINING MODULE VISIBILITY

Some languages have access modifiers that regulate the visibility of a declaration in other modules.
For example, in Rust, it is possible to write  to indicate in which module a declaration is visible.
Similarly, some languages support giving particular classes access to an item.
It is the primary accessibility mechanism for Eiffel, and 's  modifier enables this as well.
Less flexible approaches, such as Java's package visibility and 's  keyword can be seen as special instances of this mechanism.

To demonstrate how these access policies can be encoded using scope graphs, we extend our base language as follows.
<Ref> introduces an additional modifier keyword *internal, which can contain references to modules.
The declaration is visible in these modules only.
The corresponding accessibility policy has a set of scopes, each corresponding to a name given in the keyword argument.

Next, we explain how this keyword is interpreted.
An *internal declaration is accessible if the reference occurs in a module that the arguments to the *internal modifier give access to.
This is formalized in the rules given in <ref>.
Rule a-int translates an *internal access modifier to the policy.
Each module name argument to the modifier ($x_i$) is resolved relative to the current scope $s$.
This yields a collection of module scopes $s_i$, which are included in the resulting policy.
The ap-int rule encodes that accessing an *internal variable is valid if $s_m$, the scope of some enclosing module of $s$ (the scope of the reference), is in the list of scopes to which access is granted.

<Ref> gives an example of an internal variable.
Class 𝕀A has a field 𝕀x that can be accessed from module 𝕀M.
In the scope graph, this is indicated with the access policy $\MODof{\setOf{\xscoperef{M}}}$ on the corresponding declaration in $\xscoperef{A}$.
The derivation of this policy is shown in <ref>.
Module 𝕀M contains a nested module 𝕀N, which contains a class 𝕀B.
In class 𝕀B, the field 𝕀x is accessed on an instance of 𝕀A.
The (partial) typing derivation in <ref> shows this access is allowed by the ap-int rule.
The first premise asserts that $\xrootscope$, $\xscoperef{M}$ and $\xscoperef{N}$ are the enclosing modules of $\xscoperef{B}$.
This can be seen in the scope graph, as those scopes are reachable via paths with regular expression $\reclos{\lblLEX}\lblTHISMOD$ (<ref>).
As $\xscoperef{M}$ occurs both in the enclosing modules and in the access policy, access is allowed.

Variant 1.

Several variations on this scheme are conceivable.
For example, languages can restrict the modules to which an *internal modifier may expose a declaration.
For example, Rust has the *pub*(*in path*) visibility modifier, similar to how we defined *internal.
However, at the path position, only “an ancestor module of the item whose visibility is being declared” is allowed <cit.>.
This is encoded in <ref>.
Compared to a-int, this rule adds premises (highlighted) that guarantee that the arguments of the *internal modifier ($x_i$) resolve to an enclosing module ($s_i \in S_M$).

Note how these premises would make the example fail to type-check.
Only $\xrootscope$ is an enclosing module of $\xscoperef{A}$.
In particular, the derivation in <ref> would have an additional premise $\xscoperef{A} \in \setOf{s_0}$, which is clearly unsatisfiable.

Variant 2.

Next, consider the example in <ref> again.
In the system above,  is accessible in , because  is exposed to one of its enclosing modules (𝕀M).
However, $\xscoperef{M}$ is not its innermost enclosing module.
Such a more lenient accessibility scheme might be desirable (, Rust has this behavior), but languages such as Java do not allow this.
To model these languages, we instead use the premise that asserts $s_m$ is the innermost enclosing module scope.
The rule for this variant is given in <ref>.

With this addition, the example would fail to type-check as well.
The access validation (<ref>) would now have to satisfy $\premEncMI{\SG}{\xscoperef{B}}{\xscoperef{M}}$, which is impossible, as $\xscoperef{N}$ is the innermost enclosing module.

Variant 3.

Finally, consider example <ref> from the introduction again.
In this example, the reference to 𝕀x in class 𝕀C was not valid, as 𝕀B (by virtue of residing in a different package), did not inherit 𝕀x.
The (partial) rule in <ref> covers this case.
For each scope in the path (apart from the target), it adds premises that assert that the definition is exposed to that scope (similar to $s$ in <ref>).
[Alternatively, the premises of <ref> can be used when direct exposure is required.]
The target is excluded because it is not inheriting the accessed field, but rather defining it.
(Recall that paths move from reference to declaration, so the target is the scope of the defining class.)
For that reason, there is no need to assert it inherits the field.

When adding this rule fragment to the derivation in <ref>, there will be additional premises that validate that class 𝕀C inherits 𝕀x.
This is the case, as 𝕀C resides in module 𝕀M.

§ DEFINING SUBCLASS VISIBILITY

Next, we consider how to define access modifiers that regulate access from other classes:
the *private modifier (<ref>), and the *protected keyword (<ref>).

§.§ Private Access

The  access modifier is slightly challenging to define, as languages implement it differently.
For example, allows accessing private variables on instances of subclasses, whereas Java does not.
Consider the example programs in <ref>.
In the Java case, the access  is invalid, because it only allows access on instances of .

On the other hand, Java exposes  members to the outermost enclosing class[
“[When] the member or constructor is declared , (...) access is permitted if and only if it occurs within the body of the top level class [sic!] that encloses the declaration of the member or constructor." <cit.>
], while only exposes members to the defining (, innermost enclosing) class (including nested classes), as shown in <ref>.

We start with modeling the semantics

in <ref>.
Rule ap-priv states that the class in which the field is declared (which is the target of the

path $\mathsf{tgt}(p)$) should be an enclosing class of the scope in which the access occurs.
This permits access from nested classes of $\mathsf{tgt}(p)$, but does not expose it to enclosing classes.
On the other hand, access on instances of subclasses is allowed, as there are no constraints on the structure of the path.

Note that we did not specify that this rule matches on the policy specifically,
but rather applies to any access policy $A$.
This is a deliberate choice; it adds the possibility of using this rule as a fallback in case no other rule works.
This ensures other accessibility policies will never be more strict than , which corresponds to general intuition.
By matching on an arbitrary $A$ in ap-priv, we simplify the definition of the other policies, as they otherwise would need to define special rules for -like access.

Current Instance.

Now, we adapt these rules to match the Java semantics.
First, <ref> shows how to prevent access to the private field on instances of subclasses (<ref>).
It uses a new type of constraint, $\premMatchRE{p}{\re}$, which holds when the sequence of labels in path $p$ is in the language described by the regular expression $\re$.
In this case, we assert that the access path $p$ must adhere to the regular expression $\reclos{\lblLEX}$.
This prevents access from instances of subclasses of the defining class, as that requires traversing an $\lblEXT$ edge.
For example, the access path in <ref> would be $\premMatchRE{\xscoperef{B} \scopeedget[\lblEXT] \xscoperef{A}}{\reclos{\lblLEX}}$, which is not satisfiable.

Outermost Class.

Finally, <ref> shows how to expose  fields to the outermost enclosing class.
In this rule, the set $S_{C_\mathit{ref}}$ contains the scope of the enclosing classes of the reference location,
and $S_{C_\mathit{decl}}$ contains the scope of the enclosing classes of the class in which the declaration occurs.
These sets should share a scope $s_c$, which represents the shared enclosing class of the reference and the declaration.

Note how this rule enables type-checking the program in <ref>.
Using ap-priv does not work, as $\premEncC{\SG}{\xscoperef{A}}{\setOf{\xscoperef{A}}}$,
which does not include $\mathsf{tgt}(p) = \xscoperef{B}$.
However, we can check it with ap-priv2, as $\premEncC{\SG}{\mathsf{tgt}(p)}{\setOf{\xscoperef{B}, \xscoperef{A}}}$, which includes the shared enclosing class $\xscoperef{A}$.

§.§ Protected Access

The  access modifier (<ref>) grants access to subclasses of the defining class, including classes nested in subclasses.
For field access expressions (e.x), e must be an instance of a class that encloses the reference <cit.>.
This semantics (<ref>) can be modeled by asserting that there should be some class $s_c$ that is both
(a) an enclosing scope of the reference location ($\premEncC{\SG}{s}{S_C}$), and
(b) occurs in the in the access path ($s_c \in \mathsf{scopes}(p)$).
The last condition implies that the enclosing class $s_c$ is a subclass of the defining class,
which is the intuitive understanding of the  keyword.

<Ref> demonstrates how this rule works.
In this program, there is a class 𝕀A which has a subclass 𝕀B.
Class 𝕀B has a nested class 𝕀I, which has a method 𝕀f with a parameter 𝕀b of type 𝕀B.
The body of 𝕀f accesses field 𝕀x on the instance of 𝕀B.
On the right-hand side of the picture, a part of the corresponding scope graph is shown.
The scopes for classes $\id{A}$ and 𝕀B are connected by an $\lblEXT$-edge again.
The fact that class 𝕀I is nested in class 𝕀B is represented by the $\xscoperef{I} \scopeedget[\lblLEX] \xscoperef{B}$ edge, similar to other lexically nested constructs.
Likewise, scope $\xscoperef{f}$, which represents the body of the method 𝕀f, has a $\lblLEX$-edge to $\xscoperef{I}$.

<Ref> shows how the access to  is validated.
The first premise states that $\xscoperef{I}$ and $\xscoperef{B}$ are the enclosing classes of $\xscoperef{f}$.

The other premises assert that $\xscoperef{B}$ is in the enclosing classes as well as in the access path.
Together, this allows access to the protected member.
Note how access to an instance of 𝕀A in $\xscoperef{f}$ would not be allowed.
In that case, the access path would have been just $\xscoperef{A}$, which is not an enclosing class of $\xscoperef{f}$.

§ COMBINING SUBCLASS AND MODULE VISIBILITY

Access modifiers regulating both the module and subclass dimensions occur in real-world languages as well.
For example (as noticed earlier), Java's  keyword also exposes a definition in the same package, similar to 's .
In addition, has a  modifier, which allows access to subclasses in the same assembly only.
In fact, those two keywords denote the two main ways in which access modifiers can interact.
First,  denotes disjunctive interaction, where a declaration is accessible from the subclasses or the same module.
Second,  denotes conjunctive interaction, where a declaration is accessible from the subclasses in the same module only.
These interactions are straightforward to define, with one intricate case discussed below.

<Ref> defines the syntax of the two new keywords (based on their name in ) and policies.
We add (Subclass/Module, Disjunctive) and (Subclass/Module, Conjunctive) policies, which each contain a list of module scopes to which they are exposed.
The translation from keyword to policy is given in <ref>.
Both rules resolve their module arguments, similar to a-int.
The policy has one rule (ap-smc), which simply asserts that access is granted by the module () and protected () policies.
There are two rules for the policy.
The first one simply delegates to the access policy, permitting access wherever a  member would have been accessible.
The other rule delegates to the policy, but more careful attention must be paid here (hence the $(*)$ mark).
Recall that the semantics of this policy has a variant that asserts that the whole inheritance chain has access to the declaration (<ref>).
However, this extension should not be applied here, because the  part of this modifier already grants access, regardless of the module-level exposure.

§ DEFINING EXTENDS-CLAUSE ACCESSIBILITY RESTRICTION

Until now, we have only considered inheritance as it exists in Java and .
In this section, we shift our focus to , in particular the access modifiers on extends clauses.
In , it is possible to add a  modifier to an extends clause, which reduces the accessibility of  and  members to  in the derived class.
Similarly, the  keyword can be used to reduce the accessibility of  members to .
For qualified accesses, imposes the additional constraint that the inheritance chain leading to class in which the variable is declared should be accessible from the class in which the access occurs <cit.>.

In contrast to the previous sections, we cannot encode inheritance-imposed access control in our accessibility policy $A$.
Instead, we encode it in the scope graph directly.
For that purpose, we introduce two new labels: $\lblEXTPRIV$ and $\lblEXTPROT$, which model private and protected extension, respectively.
Similar to the previous sections, $\lblEXT$ will model public extension; inheritance without access restriction.

Fortunately, we can validate path access independently from the declaration-level access policy.
That also holds for the subtle interaction between  and  discussed in <ref>.
or  inheritance in subclasses of the reference class can still compromise these access modes, and must therefore be validated.
We require two adaptations to the rules t-var and t-fld (<ref>).
First, the regular expressions of the queries must be changed to also traverse these new edges.
Thus, in t-var, $\reLEX$ must be changed to $\reLEXCPP$.
Similarly, t-fld now has as regular expression instead of .
Second, we add a premise $\premMPth{\SG}{s}{p}$ to both rules.
This premise asserts that the labels in the path $p$ do not hide the accessed definition in scope $s$.

Path accessibility can be captured in two rules, shown in <ref>.
First, p-pub asserts that a path is valid when there is only public inheritance.
With this rule, the semantics of the programs that do not use private or protected inheritance has not changed.
Second, rule p-priv-prot covers the other two cases.
This rule looks intricate, but the intuition behind it is not too complicated.
Similar to the  and  modifiers (<ref>), access must occur within the class where the member is /.
This is now not necessarily the defining class, but rather the last class in the inheritance chain that has a non-public modifier on the extends clause.
In the rule, this is encoded as follows.
The first two premises introduce a scope $s_c$, which is an enclosing scope of the reference location $s$.
The third premise asserts that the path $p$ can be split into two segments at scope $s_c$.

That is, $p$ consists of two segments: a part $p_1$ from $s_1$ to $s_c$ and a part $p_2$ from $s_c$ to $s_n$.
This implies that $s_c$ is in the access path.
To validate that all subclasses of $s_c$ in the path have public inheritance, $p_1$ should match regular expression $\reclos{\lblLEX}{\lblEXT}$.
[Alternatively, one can encode the requirement that the instance type must be $s_c$ itself by using $\reclos{\lblLEX}$, similar to <ref>.]
The path leading from the current class to the declaration ($p_2$) may start with a private inheritance step ($\reopt{\lblEXTPRIV}$), but may have only public and protected inheritance higher in the access path.

<Ref> gives an example that uses this rule.
There is a class 𝕀A with a field 𝕀x.
Class 𝕀A is inherited privately by class 𝕀B, which makes 𝕀x private in 𝕀B.
Next, class 𝕀C extends 𝕀B publicly.
In class 𝕀B, 𝕀x is accessed on an instance of 𝕀C.
This access should be allowed, as class 𝕀B is the class in which 𝕀x is private as well as the class in which the reference occurs.
The partial derivation in <ref> asserts this.
$\xscoperef{B}$ is the scope that encloses the reference.
Splitting the access path from $\xscoperef{C}$ to $\xscoperef{A}$ at that $\xscoperef{B}$ yields two segments of a single step.
The segment leading up to $\xscoperef{B}$ ($\xscoperef{C} \pathstept[\lblEXT] \xscoperef{B}$) does indeed match the regular expression $\reclos{\lblLEX}\reclos{\lblEXT}$.
Likewise, the other segment also matches its regular expressions, showing that this access is valid.
Note that, when class 𝕀C would have extended class 𝕀B with  or  visibility instead,
the premise on the first section would not hold anymore.
This corresponds with the behavior in <ref> (the field must be accessible as if it was defined on the instance type) as well as the specification of cited above.

§ ANALYSIS

A comprehensive model of accessibility can be made by composing the system fragments we discussed so far (<ref>).
In this section, we discuss a few properties that our system adheres to.

§.§ Soundness of Access Policies

First, we claim some soundness theorems for ,  and  access.

There is no soundness theorem for , as access is allowed unconditionally.
Soundness theorems for  and  are easily derived from <ref>, and hence omitted.
In the theorems, $P_\SG$ ranges over valid typing derivation for an AML program with scope graph $\SG$,
$x_r$ over references, and $x_d$ over declarations.
sec:characterizing-predicatesD defines the predicates used in these theorems, and proves them.

First, soundness for  access is stated as follows:

\begin{align*}
&\mathsf{resolve}_{P_\SG}(x_r) = x_d
\mathrel{\land}
\mathsf{private}_{P_\SG}(x_d)\
\Rightarrow{}\\
\exists s_d.\
\mathsf{definingClass}_{P_\SG}(x_d) = s_d
\mathrel{\land}
\mathsf{enclosingClass}_{P_\SG}(x_r, s_d)
\end{align*}

This should be read as `when $x_r$ resolves to $x_d$, and $x_d$ is private, then $x_r$ must occur in the class $s_c$ that defines $x_d$'.

Likewise, soundness for  access is stated as:

\begin{align*}
&\mathsf{resolve}_{P_\SG}(x_r) = x_d
\mathrel{\land}
\mathsf{protected}_{P_\SG}(x_d)\
\Rightarrow {}\\
\exists s_c, s_d.\
\mathsf{definingClass}_{P_\SG}(x_d) = s_d
\mathrel{\land}
\mathsf{enclosingClass}_{P_\SG}(x_r, s_c)
\mathrel{\land}
\mathsf{subClass}_{P_\SG}(s_c, s_d)
\end{align*}

Compared to <ref>, this theorem states that $x_r$ can occur in some arbitrary subclass $s_c$ of $s_d$ if $x_d$ is .

Finally,  access is specified correctly when:

\begin{align*}
&\mathsf{resolve}_{P_\SG}(x_r) = x_d
\mathrel{\land}
\mathsf{internal}_{P_\SG}(x_d, \setVar{x})\
\Rightarrow {}\\
(\exists x,\, s_m.\
\mathsf{enclosingMod}_{P_\SG}(x_r) = s_m
\mathrel{\land}
x \in \setVar{x}
\mathrel{\land}
\mathsf{resolveMod}(x) = s_m) \lor {}\\
(\exists s_d.\
\mathsf{definingClass}_{P_\SG}(x_d) = s_d
\mathrel{\land}
\mathsf{enclosingClass}_{P_\SG}(x_r, s_d))
\end{align*}

This theorem states that references to declarations with modifier  are valid if the enclosing module of the reference $s_m$ is referred to in the arguments of the access modifier $\setVar{x}$, or if it is accessed as a private variable.

§.§ Equivalence of Access Policies

The access policy language A we defined is not minimal.
It is possible to define equivalent policies in multiple ways.
To analyze that, we define equivalence of access policies as follows:

[Equivalence of Access Policies]definitionaccesspolicyequiv

∀, s, p. (spA) ⇔(spA')
A ≡A'

That is, two accessibility policies are equivalent when, for any scope $s$, path $p$, scope graph $\SG$, either both policies admit access, or neither does.

The equivalences that hold in our model are: $\PRT \equiv \SMDof{\emptyset}$ and $\PRV \equiv \SMCof{\emptyset} \equiv \MODof{\emptyset}$.
This follows from the fact that module access grants nothing if no module parameters are given.
Thus, the $\SMDof{\emptyset}$ policy reduces to $\PRT$, while $\SMCof{\emptyset}$ and $\MODof{\emptyset}$ do not elevate accessibility beyond $\PRV$.
sec:equivalence-proofsB gives proofs for each of these equivalences.
Because of these equivalences, we did not include and in our implementation (<ref>).

§.§ Order of Access Policies

Intuitively, there exists an ordering between accessibility policies, where $\PRV$ is the bottom most restrictive, and $\PUB$ is the least restrictive.
This order is partial, as the module-exposure dimension and subclass-exposure dimension are orthogonal.
Assuming a subset relation on scope sets ($S \subset S'$), we can define a strict partial order $A <_A A'$ as follows:

plc/.style = draw=black, rounded corners,
cond/.style = yshift = 0.65em, xshift=0.1em,
node distance = 1.5em and 1em

[plc] (prv) $\PRV$;

[plc, right = of prv] (smcl) $\SMCof{S_0}$;
(smcl) edge[->] (prv);

[plc, right = 3.85em of smcl] (smcr) $\SMCof{S_1}$;
(smcr) edge[->] node[cond] $S_0 \subsetneq S_1$ (smcl);

[plc, above right = of smcr, xshift = -2em] (modl) $\MODof{S}_1$;
(modl) edge[->] (smcr);

[plc, right = 3.85em of modl] (modr) $\MODof{S}_2$;
(modr) edge[->] node[cond] (modlr-c) $S_1 \subsetneq S_2$ (modl);

[plc] (prt) at (smcr -| modlr-c) $\PRT$;
(prt) edge[->] (smcr);

[plc, below right = of modr, xshift = -2em] (smdl) $\SMDof{S_2}$;
(smdl) edge[->] (modr);
(smdl) edge[->] (prt);

[plc, right = 3.85em of smdl] (smdr) $\SMDof{S_3}$;
(smdr) edge[->] node[cond] $S_2 \subsetneq S_3$ (smdl);

[plc, right = of smdr] (pub) $\PUB$;
(pub) edge[->] (smdr);

where the edges indicate instances of the $<_A$-relation.
The edges with a condition indicate that $\SMC$, $\MOD$, and $\SMD$ become more permissive when more scopes are added to the policy.

The intuition behind this order is not arbitrary.
In fact, we claim the following:
[The order on access policies $<_A$ is well-behaved]theoremaccpolorderwellbehaved

(A <_A A')
⇒∀, s, p. (spA) ⇒(spA')

That is, when $A$ is more restrictive than $A'$, and $A$ permits access in scope $s$ via a path $p$, then $A'$ will permit that access too.
A proof of this theorem can be found in sec:preorder-proofsC.

§ EVALUATION

So far, we have motivated our specification with examples from real-world languages such as Java and , and stated some generic properties of our model.
However, for our specification to be usable as a basis for practical tools, it must correspond with the behavior of the actual languages.
To validate that, we evaluated our specification in two ways.
First, we systematically compared our specification with reference compilers of Java, , and Rust.
Second, we validated the compatibility of our framework with recent work on language-parametric code completion <cit.>.

§.§ Comparison with Reference Compilers: Implementation

The comparison to compilers of real-world languages is implemented as follows:

*  Apply our type system on an AML program (the test case).

* Translate the AML program to the target language.

*  Compile the translated program using a compiler of the target language.

* Compare results: either both analyses should succeed, or both should give errors.

We discuss these steps in more detail below.

AML Type Checker.

To compare our model with real-world compilers, we need a way to type check concrete AML programs.
To that end, we implemented AML in the Spoofax language workbench <cit.>.
The actual type system is implemented using the Statix specification language <cit.>.
Statix is a suitable choice, as its declarativity allows an overall straightforward translation from our inference.
For example, the Statix encoding of rule t-var in <ref> strongly corresponds to the original (<ref>).
Using this implementation, we can systematically check accessibility in concrete AML programs.

Compiling with Reference Compiler

Next, we implemented source-to-source translations from AML to each of Java, and Rust.
This translation was straightforward by design, as otherwise the results of the type checkers can be different due to semantic differences introduced by the translation.
For that reason, we do not support AML features that have no direct counterpart in the target language.
For example, the translation to Java will error when the AML program uses the  access modifier, as Java does not support that accessibility policy.
This way, we know that correspondence between the programs is guaranteed when the translation succeeds.

After translating, we invoke the reference compiler, observe its output (success or failure),
and compare the given output with the result from our own type checker (step <ref>).
If those are different (, our type checker accepts the program, while the reference compiler emits errors, or vice versa), the test fails.

§.§ Comparison with Reference Compilers: Test Cases

To the best of our knowledge, there exists no test suite specifically aimed at verifying the semantics of access modifiers.
For that reason, we manually created an extensive test suite.
Each test contains a class , that defines some variable  with some access modifier $A$.
Furthermore, each test contains a class , in which a reference to  occurs.
and  can be related in two different ways at the same time:

* By inheritance: either (1)  and  are actually the same class, (2) have no mutual inheritance, (3)  inherits , or (4)  inherits .

* By module position: either  and  (1) occur in the same module, or (2)  occurs in a parent/sibling/child module of .

* By class nesting: either (1)  and  are top-level classes, (2)  is nested in , (3)  is nested in , or (4)  and  have a shared enclosing class.

In addition, tests for member accesses (, ) have a receiver type .
This type must either be equal to , or inherit from it.
However, it can be related in all possible other ways to  and .
By systematically exploring all options, we derived our test suite.

We excluded cases that are
(1) impossible (,  cannot be nested in  and live in a different module at the same time),
(2) use features not supported by the target language,
(3) invalid for another reason (, inheriting from a nested class is not allowed by Java), or
(4) do not bind properly (, lexical access where  and  do not inherit from each other, and are not nested in each other),
To reduce the number of test cases, we restricted the cases that involved nested classes to have one module only.
Additionally, we only used *private, *protected and *protected internal as access modifiers in these cases.
<Ref> summarizes the results of the test suite generation.

<Ref> shows an example test case written in the Spoofax Testing Language (SPT) <cit.>.
This test validates that a private field is accessible from a nested class.
The test consists of a program (between double square brackets), and some expectations.
In this case, we expect the (Statix-based) analysis to succeed.
Moreover, we expect the  transformation to succeed.
This transformation is executing the steps in <ref>.

There are several features present in AML that were not covered by any of the reference compilers, most notably *private/*protected inheritance, and module visibility beyond what Rust supports.
To validate we cover these features to some extent, we have written 168 additional test cases.
While initially exposing a lot of edge cases, in the end all test cases succeeded.
This shows that our specification covers the languages it set out to model rather accurately.

§.§ Code Completion

One of our future goals is to use our framework to implement refactoring tools that are sound with respect to accessibility.
The most recent work in this area is done by Pelsmaeker et al. <cit.>.
They show how Statix specifications can be used to generate editor auto-completion proposals language-parametrically.
We applied auto-completion to the access modifiers in the /Java and Rust tests (152, after deduplication), and validated soundness and completeness.
That is, when the analysis succeeded, code completion should propose the current modifier at that position.
Otherwise, if the access was invalid, the modifier should not be proposed, as only less restrictive ones are valid at that position.

We consider the fact that all completion tests pass a good indication that our specification can be applied with refactoring tools in the future.
Apparently, the code completion framework is sound and complete with respect to our encoding of access modifiers.
Accessibility errors introduced by a refactoring can be fixed by generating proposals for that position,
and using the ordering from <ref> to pick the most restrictive one.

§.§ Threats to Validity

In <ref>, we briefly mentioned that the specification as presented in the paper did not model the interaction between shadowing and accessibility correctly.
Doing so would require a full path order, instead of ordering paths by a lexicographical order on labels.
subsec:full-path-orderA.1 explains how we think that could be done.
However, Statix does not support full path orders.
To work around that, we emulated this behavior using a few helper predicates.
Our test suite gives confidence we modeled it correctly, but we did not prove that the specification in Statix and the full path order are semantically equivalent.

Finally, we might have modeled incorrect/unspecified behavior if the reference compilers were incorrect.
Examples such as <ref> were derived from actual compiler behavior.
However, we could not find our interpretation of the implementation behavior explicitly specified in the JLS <cit.>.

§ EVALUATION : OLD

In this paper, we show how to define the semantics of access modifiers using scope graphs.
Throughout <ref>,
we developed semantics for the main access modifiers occurring in real-world languages.
Apart from examples and two laws, no arguments for the correctness were given.
In this section, we explain how we validated our specification.

§.§ Implementation

Ideally, we would provide a mechanized proof that our semantics of access modifiers corresponds to some reference specification.
However, this is not possible, for multiple reasons.
First, we are not aware of any other formalization of access modifiers that we can use as a reference.
Second, for some access modifiers, we explore various ways to define them, which would require multiple reference specifications.
Instead, we applied an extensive test-based approach.
We implemented a variant of AML in the Spoofax language workbench <cit.>.
In particular, we used the Statix specification language <cit.> to implement the specification we developed in this paper.
Statix is a logic language with scope graphs embedded, which allows a straightforward translation from inference rules to a full specification.
Statix can interpret a specification as a constraint program, which yields an executable type checker.
To implement the tests, we used the Spoofax Testing Language (SPT) <cit.>.
In SPT, test cases consist of an object language program (AML in our case), and a series of expectations, such as analysis succeeding or failing.

Our language is similar to the language presented in <ref>, with two major differences.
First, a few pragmas can be added to a program, which configure the type checker to use different inference rules.
In this way, we modeled the different variants for various access modifiers
Second, Statix does not have a $\premMatchRE{p}{\re}$ constraint.
We emulate this constraint as follows:

s_𝑠𝑟𝑐 = 𝗌𝗋𝖼(p)

s_𝑡𝑔𝑡 = 𝗍𝗀𝗍(p)

R ≠∅

This query finds a path from the original source to the original destination, using the regular expression from the constraint.
In an arbitrary scope graph, $R$ could not contain $p$, but some other path(s) with the same source and destination.
However, we only use this pattern for inheritance-based visibility, and we do not model multiple inheritance.
In that case, these paths are always unique, and hence these constraints equivalent.

§.§ Comparison to Reference Compilers

The most rigorous part of the evaluation was done by using compilers of Java, , and Rust as oracles.
For each of these languages, we implemented a transformation from AML, targeting that language.
Then, we executed the type checker derived from our specification, and, the reference compiler.
If both report no errors, or if both give errors, the test passes.

For the Java comparison, we translated each module to a package, and each class its own class file.
To retain access to parent packages, we insert wildcard imports to all enclosing packages in each class file.
For example, a file containing a class  will implicitly import packages  and .
In this way, we can translate all module structures to a Java equivalent.

We wrote tests manually, where each test case has some declaration  and a reference to that declaration.
To ensure we covered the behavior of the Java compiler as much as possible, we systematically wrote test cases, with the following variation points:

* access modifier of the declaration: , , default, or

* access mode: lexical (, on the implicit  instance), or on an instance of

* the defining class

* the class containing the reference

* parent class of the class containing the reference

* subclass of the class containing the reference

* relative location of access: defining class, direct/transitive subclass, or unrelated class

* relative location of enclosing module: same module as defining class, or a sibling module

All combinations of these features add up to 120 tests.
However, some combinations are infeasible.
For example, when the access mode is lexical, we cannot put the reference in a class that is not a subtype of the defining class.
Removing invalid combinations, we retain 96 tests.
We also added tests covering nested modules with (a) all access modifiers, (b) member access only (c) on instances of the defining class and a subclass (8 tests).
Finally, we validated that access to default and protected members through multiple packages is implemented correctly (18 tests; see also <ref>),
and tested that access modifiers do not influence resolution when shadowing is concerned (24 tests; see also <ref>).
In total, this yields 146 test cases, which all pass using  1.8.

In , assemblies are the unit of encapsulation for internal visibility.
For that reason, we translated modules in our program to projects, and imports to dependencies between projects.
Similar to the Java case, we implicitly added dependencies to projects corresponding to enclosing modules.
This restricts the import structure we could use in our tests, as projects cannot be mutually dependent on each other.

We automatically translated the Java tests to , and generated additional cases with  and  accessibility.
Implicitly, our test expectation switches the type checker configuration to account for the differences in  access (<ref>).
All 132 tests pass, using  7.0.401 to compile them.
Together, these tests cover the `Subclass Access Modifier' category of our feature model (<ref>).

Java and have only limited module-accessibility features.
To evaluate that aspect of our specification better, we additionally targeted Rust (1.73.0) as a reference compiler.
In 60 tests, we covered a range of relative positions of reference modules, declaration modules, and exposure level (, up to which ancestor module the definition can be accessed)

§.§ Own Tests

These translations do not cover all features discussed in this paper.
For example, we did not cover the case where an  modifier gives access to modules that are not lexical parents.
We could have emulated this with friends or with Eiffel, but neither was a straightforward target for a translation.
Second, we did not cover the inheritance accessibility restriction that occurs in .

To ensure we also cover the features that we did not validate against a reference compiler (<ref>),
we implemented 129 additional test cases.
These are mostly focussed at:
/ inheritance,
visibility to other modules than the most directly enclosing one, and
different variants of some rules, to validate whether they really covered the subtle semantic variations.
Together, the tests using reference compilers and our manually written tests provide good coverage of the specification.

§.§ Code Completion

One of our future goals is to use our framework to implement refactoring tools that are sound with respect to accessibility.
The most recent work in this area is done by Pelsmaeker et al. <cit.>.
They show how Statix specifications can be used to generate editor auto-completion proposals language-parametrically.
We applied auto-completion to the access modifiers in the /Java and Rust tests (192 total), and validated soundness and completeness.
That is, when the analysis succeeded, code completion should propose the current modifier at that position.
On the other hand, if the access was invalid, the modifier should not be proposed.
Again, all tests succeeded.

We consider this a good indication that our specification can be applied in refactoring tools in the future.
Accessibility errors introduced by a refactoring can be fixed by generating proposals for that position,
and using the ordering from <ref> to pick the most restrictive one.

§.§ Performance

Small check on performance

- Performance: not comparable to hand-written type checkers, but usable in practice

- compare performance with and without access checking

§ RELATED WORK

In this section, we discuss previous work related to access modifiers and scope graphs.

§.§ Access Modifier Semantics and Implementations

The origin of access modifiers dates back to at least Simula 67,
which around 1972 introduced  and  access modifiers <cit.>
(the latter being equivalent to our ).
Later, languages such as Java and incorporated these keywords, making them well-known and often used.
Design principles and patterns <cit.> using these keywords were developed,
making contemporary software development heavily reliant on accessibility features the programming language provides.

Giurca and Savulea (2004) <cit.> apply object-oriented notions of ,  and  to logic programs,
with the purpose of better knowledge distribution and run time optimization.
Moreover, Apel et al. <cit.> introduce access modifiers in feature-oriented programming.
Where we define accessibility for module nesting and class inheritance, they add the `feature refinement' dimension to this.
In particular, the  keyword restricts access to the `current feature' only (comparable to  in the class inheritance dimension),
the  keyword grants access to the current feature and later refinements (comparable to ), and
the  modifier allows access from any position (similar to ).
In our terminology, their model supports `conjunctive' combination of the class and feature dimensions.
As <ref> shows that combining the module and class dimensions conjunctively is straightforward,
we expect that integrating their work in our model will not pose major challenges (apart from a combinatorial explosion of policies).

As access modifiers mainly originated from practical needs, it is not very surprising that little attention to them was paid from a more theoretical perspective.
A few attempts to create a more formal account have been performed, however.
In 1998, Yang <cit.> presented a formalization of Java access modifiers using attribute grammars.
At that time, attribute grammars still lacked several convenience features, such as default attributes <cit.> and collection attributes <cit.>.
For that reason, all members must be propagated explicitly to the scopes where they are accessible,
which makes the specification rather verbose.
Additionally, since fields and methods are not treated equally (shadowing vs. overriding), they are treated separately, doubling the specification size.
In contrast, we specify the propagation of members queries in scope graphs, which is more concise.
The additional requirements on methods (not explicitly discussed), can be handled at the definition site.
Furthermore, we cover more features than just the Java ones.
Fharkani et al. <cit.> present a generalized model of accessibility,
where accessibility is modeled as a set of rules granting access of a member to another member (similar to Eiffel/ in ).
In addition, rules can deny access to the named member, or apply to all members except the named ones.

Steimann et al. <cit.> observe that disregarding accessibility can result in a lot of subtle mistakes.
For example, a method may silently fail to override another method when it is moved to a different package,
which results in different dynamic dispatch.
To capture these errors, they present nine constraint generation rules that model the accessibility semantics of Java.
Refactoring tools can use these constraints to detect where the accessibility level of a member must be elevated.
This work was incorporated in the JRRT refactoring tool <cit.>, which was evaluated on a large number of real-world Java projects, showing the accuracy of their implementation.
While their work also covers overriding-specific constraints, which our specification treats rather superficially,
we think our model is more comprehensible, and also gives insight in the differences between languages.
Moreover, their work is applied in real refactoring implementations, while the quest for Statix-based refactorings is still ongoing.
Meanwhile, a similar approach was applied to Eiffel accessibility <cit.>.

While these tools elevate accessibility if needed, a different line of research aims to restrict accessibility if possible <cit.>.
The purpose of these tools is to detect access modifiers that are more lenient than needed, and restrict those.
This is claimed to improve readability, enable optimizations, and increase modularity <cit.>.
The exact underlying model is not the topic of these publications, and hence remains unclear.
Despite that, the tools appear to be useful in practice.
Zoller and Schmolitzky mention some challenges in porting their tool to other object-oriented languages <cit.>.
A language-parametric model such as ours helps in that regard by
(1) making differences between languages explicit, and
(2) make implementations of these (kind of) tools language-parametric.

§.§ Scope Graphs

Scope Graphs (<ref>) have been introduced by Neron et al. <cit.>, and later refined by Van Antwerpen et al. <cit.> and Rouvoet et al. <cit.>.
In order to bridge the gap between language specification and implementation, scope graphs have been embedded into the NaBL2 constraint language <cit.>.
Later, the Statix logic language was introduced <cit.>, which is more expressive than NaBL2.
Both languages allow specifying type checking as constraint programs, giving the language a declarative appeal, but also yielding an executable type checker.
Scope graphs are also available in a framework for concurrent and incremental type checkers <cit.> and an embedded DSL in Haskell <cit.>.
Finally, Statix specifications have been used for language-parametric code completion <cit.> and refactorings <cit.>.
Zwaan and Van Antwerpen provide a detailed overview of the development history of scope graphs, their embeddings in type system specification DSLs, and their applications <cit.>.

§ CONCLUSION

Access modifiers occur in many real-world languages.
To implement high-quality tooling for these languages, a good understanding of access modifiers is required.
In this paper, we presented a model for access validation based on scope graphs.
Our model covers the most important accessibility features in contemporary languages, including module accessibility, and inheritance accessibility, both on declarations and extends-clauses.
Variations between different languages, both in supported features and their semantics, are made explicit in our model.
Our specification is quite declarative, partly because scope graphs abstract over low-level name resolution and scoping details.
Our model was validated using an extensive test suite, using Java, , and Rust compilers as oracles.
This test suite was also used to show that we can synthesize access modifiers accurately using previous work on code completion <cit.>.

Our main motivation for this work is twofold.
First, we aim to provide a `language-transcendent' model for accessibility that enables comparison of different languages regarding accessibility.
To this end we identify and formalize differences in the semantics of several access modifiers.
In addition, we formulate soundness theorems of several access modifiers, and prove them.
As such, we consider our specification accurate enough to serve as a reference for future tool implementations.
Second, we aim to use our model in language-parametric refactorings, ensuring they respect accessibility properly.
As these refactoring tools are still in development, actual validation of this application is still future work.

*proofsketchbaseProof Sketch