Defining Name Accessibility using Scope Graphs (Extended Edition)

TL;DR

This paper introduces a formal, language-independent model for defining name accessibility in programming languages using scope graphs, enabling precise specification and synthesis of access modifiers across multiple languages.

Contribution

It presents a declarative, executable model for name accessibility based on scope graphs, applicable to various languages, and demonstrates its correctness and utility in synthesizing access modifiers.

Findings

Model accurately matches compiler accessibility policies

Successfully synthesizes access modifiers in programs with holes

Provides a uniform approach for different language policies

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.