Many existing systems track aliasing and uniqueness, each with their own trade-off between expressiveness and developer effort. We propose Latte, a new approach that aims to minimize both the amount of annotations and the complexity of invariants necessary for reasoning about aliasing in an object-oriented language with mutation. Our approach only requires annotations for parameters and fields, while annotations for local variables are inferred. Furthermore, it relaxes uniqueness to allow aliasing among local variables, as long as this aliasing can be precisely determined. This enables support for destructive reads without changes to the language or its run-time semantics. Despite this simplicity, we show how this design can still be used for tracking uniqueness and aliasing in a local sequential setting, with practical applications, such as modeling a stack.

翻译：许多现有系统追踪别名与唯一性，各自在表达能力与开发者投入之间权衡。我们提出Latte，一种旨在最小化对象语言（含可变性）中别名推理所需注解数量与不变量复杂度的新方法。该方法仅需对参数和字段进行注解，而局部变量的注解则自动推断。此外，它放宽了唯一性约束，在别名可精确确定的前提下允许局部变量间的别名关系。这在不修改语言及其运行时语义的情况下支持破坏性读取。尽管设计简洁，我们展示了如何将该方案用于局部顺序环境中的唯一性与别名追踪，并实现诸如栈建模等实际应用。