Saved in:
Bibliographic Details
Main Authors: Zwaan, Aron, Poulsen, Casper Bach
Format: Preprint
Published: 2024
Subjects:
Online Access:https://arxiv.org/abs/2407.09320
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866914867782352896
author Zwaan, Aron
Poulsen, Casper Bach
author_facet Zwaan, Aron
Poulsen, Casper Bach
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2407_09320
institution arXiv
publishDate 2024
record_format arxiv
spellingShingle Defining Name Accessibility using Scope Graphs (Extended Edition)
Zwaan, Aron
Poulsen, Casper Bach
Programming Languages
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.
title Defining Name Accessibility using Scope Graphs (Extended Edition)
topic Programming Languages
url https://arxiv.org/abs/2407.09320