论文标题
报春花：通过其属性选择容器数据类型
Primrose: Selecting Container Data Types by Their Properties
论文作者
论文摘要
上下文：容器数据类型无处不在，使开发人员可以通过易于使用的编程接口有效地存储和处理数据集合。许多编程语言基于提供不同功能和性能特征的数据结构，在其标准库中提供了各种容器实现。 查询：为应用程序选择 *最佳 *容器并不总是很简单，因为在不同的情况下，性能特征可以在不同的情况下发生巨大变化，并且由于现实世界的性能并不总是与理论复杂性相关。 方法：我们提出了Primrose，这是一种语言无关工具，用于从一组满足应用程序开发人员提供的 *属性 *的容器数据类型中选择最佳性能有效的容器实现。 Primrose会自动选择由容器库开发人员编写的 *库规格 *的有效容器实现集，可满足指定的属性。最后，原始人根据其运行时性能对有效的库实现进行排名。 知识：借助报春花，应用程序开发人员可以将容器的预期行为指定为具有 *语义属性 *的类型改进，例如，如果容器应仅包含唯一值（例如``set''），或者应满足``stack''的lifo属性。语义属性很好地补充 *句法属性 *（即特质，接口或类型类），允许开发人员在不承诺实现混凝土实现的情况下指定容器的编程接口 *和 *行为。 接地：我们介绍了预处理的原型实现，该原型实现了预处理的锈蚀代码，选择有效的容器实现并将其对其性能进行排名。然而，初月的设计是语言敏捷的，并且易于集成到支持容器数据类型和特征，接口或类型类的其他编程语言中。我们的实现将属性和库规范编码为rosette中的验证条件，这是SMT求解器的接口，该界面确定了有效的容器实现的集合。我们通过指定几个容器实现来评估报春花，并测量为选择与求解器的各种属性组合选择有效实现所花费的时间。我们自动通过基于属性的测试来验证该容器实现符合其库规格。 重要性：这项工作提供了一种新颖的方法，可以将容器类型的抽象建模和规范直接带入程序员的工作流程中。应用程序编程人员现在可以在规范的级别上工作，而不是选择具体容器实现，而只是说明他们从容器类型中所需的行为，并且可以自动选择最佳的实现。
Context: Container data types are ubiquitous in computer programming, enabling developers to efficiently store and process collections of data with an easy-to-use programming interface. Many programming languages offer a variety of container implementations in their standard libraries based on data structures offering different capabilities and performance characteristics. Inquiry: Choosing the *best* container for an application is not always straightforward, as performance characteristics can change drastically in different scenarios, and as real-world performance is not always correlated to theoretical complexity. Approach: We present Primrose, a language-agnostic tool for selecting the best performing valid container implementation from a set of container data types that satisfy *properties* given by application developers. Primrose automatically selects the set of valid container implementations for which the *library specifications*, written by the developers of container libraries, satisfies the specified properties. Finally, Primrose ranks the valid library implementations based on their runtime performance. Knowledge: With Primrose, application developers can specify the expected behaviour of a container as a type refinement with *semantic properties*, e.g., if the container should only contain unique values (such as a `set`) or should satisfy the LIFO property of a `stack`. Semantic properties nicely complement *syntactic properties* (i.e., traits, interfaces, or type classes), together allowing developers to specify a container's programming interface *and* behaviour without committing to a concrete implementation. Grounding: We present our prototype implementation of Primrose that preprocesses annotated Rust code, selects valid container implementations and ranks them on their performance. The design of Primrose is, however, language-agnostic, and is easy to integrate into other programming languages that support container data types and traits, interfaces, or type classes. Our implementation encodes properties and library specifications into verification conditions in Rosette, an interface for SMT solvers, which determines the set of valid container implementations. We evaluate Primrose by specifying several container implementations, and measuring the time taken to select valid implementations for various combinations of properties with the solver. We automatically validate that container implementations conform to their library specifications via property-based testing. Importance: This work provides a novel approach to bring abstract modelling and specification of container types directly into the programmer's workflow. Instead of selecting concrete container implementations, application programmers can now work on the level of specification, merely stating the behaviours they require from their container types, and the best implementation can be selected automatically.
