Defining Name Accessibility using Scope Graphs (Extended Edition)

TL;DR

This work tackles the challenge of formalizing name accessibility across languages by modeling accessibility as predicates over resolution paths in scope graphs. It introduces AML, a base language whose type system integrates access control via scope-graph queries, and extends AML to cover modules, subclasses, and extends-clause restrictions, including private/protected/internal interactions. The model is implemented in Statix and validated against reference Java, C#, and Rust compilers, with a substantial test suite and evidence that AML can guide language-parametric refactorings and code completion. The approach provides a language-transcendent framework for reasoning about accessibility features, enabling precise comparisons and sound tool support across languages and future refactoring work.

Abstract

Many programming languages allow programmers to regulate accessibility; i.e., annotating a declaration with keywords such as export and private 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, C#, C++, 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 C#, Java, and Rust compilers, and show we can synthesize access modifiers in programs with holes accurately.

Figures (27)

• Figure 1: Examples of intricate Access Modifier semantics. Classes are assumed to be public.
• Figure 2: Re-exports can change Accessibility
• Figure 3: Feature Model for Access Control.
• Figure 4: Reachability example. The $\mathsf{{\mathsf{IMP}}\xspace}^{?}$ part in the regular expression prevents traversal over the second ${\mathsf{IMP}}\xspace$ edge.
• Figure 5: Shadowing example. The highlighted label order causes the edge to $\raisebox{0.1em}{$s_{\texttt{F}}$}$ to have priority.

Theorems & Definitions (45)

• Theorem 1: Soundness of private member access
• Theorem 2: Soundness of protected member access
• Theorem 3: Soundness of internal member access
• Definition 3: Equivalence of Access Policies
• Theorem 4: The order on access policies $<_A$ is well-behaved
• Definition 4: Equivalence of Access Policies
• Lemma 5
• Lemma 6
• Lemma 7
• Theorem 8