基于作用域图的名称可访问性定义（扩展版）
Defining Name Accessibility using Scope Graphs (Extended Edition)
AI总结：
针对现有类型系统缺乏名称可访问性形式化描述的问题，提出基于作用域图的语言参数化可访问性模型，在Statix中实现并验证了其正确性与访问修饰符合成能力。
摘要：
许多编程语言允许程序员调控可访问性，即通过export、private等关键字标注声明，指明其可被访问的范围。尽管名称可访问性对编译器、编辑器自动补全与工具链、自动化重构等场景至关重要，但现有类型系统中，很少有对名称可访问性的形式化描述。\n我们提出了一种声明式、可执行且语言参数化的名称可访问性模型，该模型为Java、C#、C++、Rust和Eiffel中的名称可访问性提供了形式化规范。我们通过将名称可访问性定义为作用域图解析路径上的谓词来实现这一点。由于作用域图是一种语言无关的名称解析模型，我们的模型为不同语言定义不同的可访问性策略提供了统一方法。\n我们的模型在Statix中实现，Statix是一种使用作用域图进行可执行类型系统规范的逻辑语言。我们在一个测试套件上评估了其正确性，将其与C#、Java和Rust编译器进行了比较，结果表明我们能够在带空缺的程序中准确合成访问修饰符。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
