首页> 外文会议>ECOOP 2011 - Object-oriented programming >Tunable Static Inference for Generic Universe Types
【24h】

Tunable Static Inference for Generic Universe Types

机译:通用宇宙类型的可调静态推理

获取原文
获取原文并翻译 | 示例

摘要

Object ownership is useful for many applications, including program verification, thread synchronization, and memory management. However, the annotation overhead of ownership type systems hampers their widespread application. This paper addresses this issue by presenting a tunable static type inference for Generic Universe Types. In contrast to classical type systems, ownership types have no single most general typing. Our inference chooses among the legal typings via heuristics. Our inference is tunable: users can indicate a preference for certain typings by adjusting the heuristics or by supplying partial annotations for the program. We present how the constraints of Generic Universe Types can be encoded as a boolean satisfiability (SAT) problem and how a weighted Max-SAT solver finds a correct Universe typing that optimizes the weights. We implemented the static inference tool, applied our inference tool to four real-world applications, and inferred interesting ownership structures.
机译:对象所有权对于许多应用程序都是有用的,包括程序验证,线程同步和内存管理。但是,所有权类型系统的注释开销妨碍了它们的广泛应用。本文通过提出通用宇宙类型的可调静态类型推断来解决此问题。与经典类型系统相反,所有权类型没有单个最一般的类型。我们的推论通过启发式方法在合法类型中进行选择。我们的推论是可调的:用户可以通过调整试探法或通过为程序提供部分注释来指示对某些类型的偏好。我们将介绍如何将通用宇宙类型的约束编码为布尔可满足性(SAT)问题,以及加权Max-SAT求解器如何找到优化权重的正确宇宙类型。我们实现了静态推断工具,将推断工具应用于四个实际应用程序,并推断了有趣的所有权结构。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号