发表机构
Software Institute, USI – Università della Svizzera italiana（软件研究所，瑞士意大利语区大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
提出Ranger系统，通过双向类型推断和轻量级流敏感分析，减少整数范围细化类型的注解负担，有效验证数组边界等属性。
AI 中文摘要
细化类型是一种静态验证技术，旨在增加传统类型系统的表达能力，同时保持易用性和自然性。虽然基于细化类型的系统已经为几种主流语言开发，但它们的实际应用仍然受到注解开销的限制，这通常比使用Java或Scala等语言的“普通”类型注解的负担更重。为了改进现状，本文介绍了Ranger：一种细化类型系统，旨在保持较小的注解开销，并与变量和循环等命令式结构无缝集成。顾名思义，Ranger专注于整数范围类型：一种特定类型的细化类型，表示有界整数范围。此类类型广泛用于验证正确的索引操作和边界内数据访问等。为了结合表达力和简洁性，Ranger基于双向类型系统，该系统运行类型推断算法，为类型检查过程提供有助于减少用户编写辅助注解需求的信息。Ranger还集成了其他形式的轻量级流敏感静态分析技术，这些技术无需显式注解即可精确捕获程序行为。我们在Licorne实验性编程语言之上实现了Ranger。我们的实验表明，Ranger的实现可以简洁地表达和验证各种有用的属性，这些属性超出了Java和Scala等标准静态类型系统的能力，并且Ranger与其他扩展类型系统（如Java Checker Framework和Liquid Java）相比具有优势，这些系统也可以检查关于范围的属性。
英文摘要
Refinement types are a static verification technique that aims at increasing the expressivity of traditional type systems while remaining easy and natural to use. While systems based on refinement types have been developed for several mainstream languages, their practical adoption remains limited by their annotation overhead, which is often a more significant burden than when using the "plain" type annotations of languages like Java or Scala. To improve the state of the art, this paper introduces Ranger: a refinement type system designed to keep the annotation overhead small and to seamlessly integrate with imperative-style constructs like variables and loops. As the name suggests, Ranger focuses on integer range types: a particular kind of refinement types that express bounded integer ranges. Such types are widely useful to verify correct index manipulation and in-bounds data accesses, among others. To combine expressiveness and succinctness, Ranger is based on a bidirectional type system, which runs a type inference algorithm to provide the typechecking pass with information useful to reduce the need for user-written auxiliary annotations. Ranger also integrates other forms of lightweight flow-sensitive static analysis techniques that precisely capture the program's behavior without explicit annotations. We implemented Ranger on top of the Licorne experimental programming language. Our experiments show that Ranger's implementation can concisely express and verify a variety of useful properties that fall beyond the capabilities of standard static type systems like those of Java and Scala, and that Ranger compares favorably to other extended type systems, such as the Java Checker Framework and Liquid Java, that can also check properties about ranges.
